benchmark.py modified: after a test additional resultfiles (xml) are created, one for each sourcefile-block. these new files are named "<benchmark>.<date>.results.<test>.<key>.xml" where "key" is the name (or the index) of the block.
example-xml "safe_sv-comp.xml" added. this file exists of only 2 tests, but 6 blocks, so 14 files are created.
6124
loewe
added option analysis.checkSoundness, defaulting to false, which, when enabled, ensures that the sound-flag of the analysis really is "true". I'd think this has to be done always, but I am not terribly sure about that - hence, implemented as option for now (maybe the order of cases in CPAchecker::analyzeResult is just wrong). However, without this, cbmc may fail with parsing/out-of-memory on a *spurious* counter-example, but CPAchecker would still say "UNSAFE", which is not correct under the specification, that the user obviously wanted a (valid) second opinion
6123
friedber
benchmark.py: correct output of filename (without commonprefix) if running several threads.
6122
friedber
benchmark.py: python3-support again, some cleanup.
6121
friedber
benchmark.py bugfix: if the executable of a tool was not found , the script was hanging (all workers were killed and the main-thread never exited, because work was not done). now the tool is searched before starting some worker, so the error can be handled.
6120
pwendler
Add option --correct-only for filtering out wrong results in the tables. This is especially useful for creating CSV files without values for wrong/unknown results. This option does not affect the score and status columns, only those columns with measurements.
6113
pwendler
fix generating C code for "sizeof(var)", was "sizeofvar"
6112
friedber
NamedRegionManager: adding function to dump a region in dot-format. this allows a representation of a bdd as graph. this method differs from the bdd-internal printDot-method, because names are printed into the nodes.
6111
loewe
bug fix: reached-set threshold were always checked, even if threshold was deactivated - no wrong behaviour but led to worse runtime
6108
friedber
benchmark.py: better handling of feaver-errors.
6107
friedber
benchmark.py: adding support for a very old tool: feaver (modex), a wrapper for spin. currently nearly all sourcefiles result in errors. In the commited benchmark-xml there are a few sourcefiles, most of them have correct results.
feaver has some basic problems: - only one function per file allowed, it must be named 'main'. - do not use labels, gotos and structs.
6106
friedber
BDDCPA: bugfix: functions can have more params, and some cleanup.
6105
friedber
BDDCPA: handle functionreturns. therefore a new variable is introduced, that contains the returnvalue.
6104
friedber
add function for equality and disequality in RegionManager.
6103
pwendler
Improve file handling: - remove global variable with path - close logfile after it was read - catch errors during logfile reading and continue - fix base path of logfile (its relative to the input file, not the output path)
6102
friedber
BDDCPA: handle functioncalls. therefore variables a managed with a stack.
6101
stieglma
changed #handleSimpleDeclaration, deleted #leave and combined their tasks in a new method, which is called by #getGlobalDeclarations (this is necessary for checking on duplicate declarations later on)
6099
stieglma
fixed a bug in #createDeclaration so duplicate declarated global variables are not renamed anymore
6098
friedber
BDDCPA: handle declarations of variables (example: "int x=0;").
6097
friedber
BDDCPA: if assignment cannot be evaluated, it can not be used (NullPointer). handle binaryExp with "<" or ">" and unaryExp with "-", instead to ignore them.
6096
friedber
BDDCPA: the region for assumptions and the right side of assignments can be created with the same method, so code was simplified. this also allows to handle assignments like "a=!b;" and "a=b&&c;".
6095
friedber
BDDCPA: handle assignments of a variable to another variable (example: "x=y;").
6094
friedber
BDDCPA: ignore assumptions like "a==num" where "num" is not zero. this type of assumption can produce wrong results, example: " int a=3; if (a==4) goto ERROR; "
6093
friedber
BDDCPA: multiple assignments to variable possible.