Create temporary branch for testing the removal of IASTNode#getRawSignature()


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/rawsignature-removal@5157 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removal of IASTNode#getRawSignature in every file and also from the constructors if necessary

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/rawsignature-removal@5160 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Merge branch 'master' into rawsignature-removal

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/rawsignature-removal@5163 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fix compile errors introduced through merge

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/rawsignature-removal@5164 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
merge changes from trunk


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/rawsignature-removal@5172 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add option cpa.predicate.smtinterpol.furtherOptions to allow pass-through of options
to the SMT solver SMTInterpol
(just like the similar option for MathSAT does).


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12259 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Created own class for the option that enables the creation of symbolic values

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12260 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Fixed a bug where the analysis was unsound when a struct was reassigned.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12261 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Fixed a bug where the analysis was unsound when the same element of a struct was used both directly (.) and via a pointer to the struct (->).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12262 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA / InvariantGeneration: The specification used for BMC+k-induction is now passed on to the invariant generation and the invariant generation uses the same specification for determining interesting variables now instead of using the default specification.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12263 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New version of SoSy-Lab Common library.
This version contains a new annotation processor
that does compile-time checks for the correct usage of @Option and
@Options.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12264 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Switch to LogManager interface in org.sosy_lab.common.log package
and organize imports.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12265 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
When using BMC+k-induction and generating additional supporting invariants, if the invariant generation itself is sufficient to prove a program correct, a shortcut is used to simplify the expensive inductive step.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12266 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added missing @Option description

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12267 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Do not create .pyc files in cloud mode on the worker (they are
irrelevant there).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12268 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Sometimes we fail to remove cgroups because they are remaining
processes. In this case we should just log, and do not let the script
crash.
This should fix the problem with the missing results in cloud mode
(where the "-" appeared in tables).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12269 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Apply benchmark-program renaming (unreach-label -> unreach-call)
to the files that are excluded in our local benchmark sets.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12270 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
benchmark-script collects more energy-values. this feature is only available on pc1-8.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12271 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add switch --all-columns to table-generator.py that shows all columns,
including those that are marked as hidden.
These columns do not appear in the output now by default.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12272 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Update to current version of AppEngine SDK.

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