Add package info for Java and C cfa type packages. 


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13102 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added Javadoc for Java type classes



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13103 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Correct check for correct class visibility in JClassType



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13104 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
bug fix: for the DEFAULT option of prefix preference in ErrorPathClassifier, an incomplete error path was returned, leading to bad interpolants in some cases

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13105 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
With Sylvan, we are allowed to call deref(bdd) in parallel.
Use this to free BDDs that were found by the GC in a separate thread,
such that we do not need to check for to-be-freed BDDs
on every operation in the main thread.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13106 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Update to newest version of JSylvan.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13107 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove the possibility to enable the memory-safety checks
of the predicate analysis via configuration options.
These checks were too expensive and never used anyway.
If one wants to use these checks again,
they should be enabled via the automata specifications
and not via configuration options.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13110 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
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