Java test file for switches tests fall-throughs now.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13887 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Resolve expressions with missing information on the right hand side in Value Analysis (for example global field accesses in binary operations)



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13888 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Correct comments in Java test program


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13889 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Reformat Java test programs.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13890 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SyntaxError contains a syntax error again


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13891 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add Java test case for Array length.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13892 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add Java test program for initial values of fields.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13893 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add char and boolean types to Java test program for initial values of fields.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13894 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Get correct initial values for global declarations in Value Analysis.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13895 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Enum comparison in Value Analysis is handled by AbstractExpressionValueVisitor, not as a special case


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13896 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
lazy initialisation of RationalMgr in MgrView, because Princess does not support Rational-theory. Also changing StringLiterals from type Rational to Int.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13904 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
No use of RationalMgr in MgrView, if it is not available. Fixing PrincessUtil, special cases are not needed.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13905 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Correct expected behaviour of Java test program FunctionCall2 from expected 'FALSE' to 'TRUE' and correct comment.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13907 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Simplify value calculation of enum comparison in Value Analysis.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13908 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Change string in statistics output to be correct for both C and Java programs.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13909 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Small fix for Z3. Using the declaration of app-term instead of the app-term itself avoids a few crashes with Z3.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13910 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Correct class name of previously renamed file FunctionCall2_true_assert.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13911 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improved CProgramScope for cases where a local variable needs to be looked up via its simple (non-qualified) name and its function name is unknown by collapsing identical duplicates.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13915 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding new method into InterpolatingProver, that returns an inductive sequence of interpolants directly from the underlying SMT-solver. There seems to be no difference (in verification-results) towards the current iterative approach, that uses the same proof for interpolating all sublists of formulas.

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