Parser: Extended the functionality of parseStatements.

Changed the interface of CParser, Scope is now requiered, but may be an
empty CProgramScope. 

Added Scope interface to be able to reuse generated types when parsing
single statement.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12962 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Parser: Fixed error in test, return simple name when requesting
qualified name without giving a function scope.

Note: Original empty FunctionScope returned "::<simple_name>"

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12963 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Parser: Fixed null pointer. names are sometimes null. qualified names
are not unique.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12964 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
cleanup and adding assertion for documentation

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12965 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
restructured to correctly work in PCC context

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12966 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed the edge from the loop head to the initial subgraph and added an initializer for the artificial program counter value.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12967 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Added the function pointer CPA to the standard configuration.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12968 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: Extended the representation by the "Exclusion" formula. This allows for storing inequalities in the environment.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12969 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug in the BMC-induction algorithm where the derived loop invariants were assumed to be stronger than they actually were.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12971 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug in BMC-induction where an unsound SAFE result was reported when the target location was syntactically unreachable from the loop head.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12972 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a synchronization issue in BMC+induction.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12973 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug in the single loop transformation introduced by a recent change: The initial subgraph actually must be syntactically reachable from the loop head, otherwise there might be multiple loop entry edges, which is not supported by the LoopstackCPA.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12975 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removed the hack introduced in revision r12132, because it has successfully been replaced with the additional loop invariant guessing introduced in revision r12894.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12976 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
update benchmark, now only contain one run for each partial certificate evaluation, considering strategy with smallest certificate which can successfully be verified

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12977 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
benchmark for parallel validation of certification, total and partial certificate

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12978 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
InvariantsCPA: When determining syntactically reachable target locations, it should be okay to skip recursion.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12980 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Some refactoring on the BMC/k-induction algorithm.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12981 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Output message if -heap is not specified
asking for more RAM.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12982 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding new parameter 'rlimits' for tool-cmdline. It can/will be used to set limits for the tool directly in the cmdline. also see #156 .

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@12983 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
if no explicit time-limit is given for a CPAchecker-benchmark, use the soft-time-limit from the benchmark-xml.

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