SMGState does not need to implement Targetable,
it had only an effect if an automaton was used to check for memory
safety problems, in which case it is not necessary
(because the automaton itself then signals that a target state has been
found).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13111 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
In automata, support $location in addition to $line as a place holder for the current program location (including file name, if necessary).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13112 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove the enum ViolatedProperty with hard-coded possible properties
to be violated.
Instead, there is now a string which should contain the human-readable reason
for the result unsafe,
and it is expected that the specification automata are used
to declare these reasons
(so that none of them appears in the actual source code of CPAchecker).
Furthermore, another advantage is that the message can be more flexible,
e.g., contain the line number.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13113 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Possibility to specify the description of the violated property in the specification automaton.
This description is given to the user in case of a specification
violation, and may include details such as the line number.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13114 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
The failure of an assert is expressed differently (with different function
calls) depending on the version of the stdlib in use. 



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13119 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Violated specification: One line for each property that is violated.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13120 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Made the SV-comp spec more general applicable. We might discuss if we should
make a new version of this spec with this modification.




git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13121 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
also let the Use-Def-Refiner make use of the prefix-selection heuristic; leads to a major improvement

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13126 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add the Guava testlib library,
a great tool for unit tests.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13127 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Create an own data class for the result of the PrecisionAdjustment.prec
method instead of using Triple.
This is shorter and easier to read code,
and provides more semantics than a plain triple.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13128 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
corrected unknown configuration

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13129 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
also allowed heuristic in partitioned based certification

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13130 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Revert commit 13120 (Violated specification: One line for each property that is violated.)
in agreement with its author.

The author id of the commit was wrong,
and there were also a few things that need to be fixed,
like the broken integration in our benchmark script).


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13132 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
For AbstractBAMBasedRefiner.computePath() return null
instead of an empty dummy ARGPath when no path can be constructed.
The method computePath is allowed to return null anyway,
there dummy element was compared with ==
(so it can be replaced with null, too, because nothing relied on its
additional methods),
and empty paths are going to be forbidden.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13133 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Make ARGPath immutable.
Having this class mutable was a very bad design,
because we use it to communicate between components,
and we store it for an extended amount of time in sets of
counterexamples.

Unfortunately, some components rely heavily on mutating ARGPaths.
Thus, a new class MutableARGPath is added that is a copy of the old one,
and these components now use MutableARGPath.
However, converting between ARGPath and MutableARGPath costs O(n)
in the length of the path each time.
Over time most of the use cases of MutableARGPath should probably
be rewritten to use only ARGPath or simple lists of states and edges.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13134 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
minor optimization for interpolation process

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13142 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fixes errors/assertions from buildbot, triggered by previously committed optimization

the AssumptionUseDefinitionCollector is still incomplete (e.g., does not take structs into account), thus, the optimization might produce too weak, even empty interpolants when fields of structs are relevant to errors

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13143 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Let the table-generator script directly compute the number of
regressions.
Previously the BuildBot would compute this number from a summary of the
results which was imprecise (if one file became better and one worse,
it would have not detected the regression).

Also add an option that allows to ignore new timeouts,
if there has been a timeout for this file before in one of the other
runs.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13144 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove five nonterministic tasks from ldv-unsafes

They reach time limit nondeterministically

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13145 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Specify a fixed small heap size for integration-simpleTests,
otherwise the amount of memory Java uses depends on the RAM of the machine.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13146 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c