Thread identification #212
Conversation
…, improve handling of external library calls
|
Can you check in the C source for the two examples please |
|
It already exists for 'basic_assign_pthread' and never existed for the 'pthread' example (someone else committed it but without the source) which is why I removed it. |
|
Oh ok my mistake, I thought it was a newly added example |
|
This obviously needs to wait for #204 to be merged in. |
| case _ => | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
This could be written in a functional style (since we have the iterator defined on the IR program you can do program.collect{}) but its still pretty interpret-able as is.
| if (threadTargets.size > 1) { | ||
| // currently can't handle case where the thread created is ambiguous | ||
| throw Exception("can't handle thread creation with more than one possible target") | ||
| } |
There was a problem hiding this comment.
Since all we currently do is output extra programs to verify we can probably just attempt to resolve all the targets and add them as separate threads.
| @@ -78,9 +85,9 @@ object Main { | |||
| val q = BASILConfig( | |||
| loading = ILLoadingConfig(conf.inputFileName, conf.relfFileName, conf.specFileName, conf.dumpIL, conf.mainProcedureName, conf.procedureDepth), | |||
| runInterpret = conf.interpret.value, | |||
| staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot)) else None, | |||
| staticAnalysis = if conf.analyse.value then Some(StaticAnalysisConfig(conf.dumpIL, conf.analysisResults, conf.analysisResultsDot, conf.threadSplit.value)) else None, | |||
There was a problem hiding this comment.
Could have --threads imply --analyse
…dures within threads
# Conflicts: # src/main/scala/ir/Program.scala
Splits threads into separate boogie output files. Currently only works for pthreads (support for other thread libraries can be added later)
-tflag enables this functionality and requires the--analyseflag to be used alongside it.