new package util.ci with
- AppliedCustomInstruction
- AppliedCustomInstructionParser
- AppliedCustomInstructionParsingFailedException
- CustomInstructionApplications

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14791 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added comments to all classes of the package util.ci

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14794 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy iteration: simplify delegation.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14799 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
LinearExpression class: tests, refactorings, bugfixes.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14800 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
LinearExpressions: updated package-info.

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

 - new model for comparing the states
 - matching traces

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

Carry the information about the pointers across the abstraction.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14806 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
during feasibility checks, only call abstraction if the (configurable) precision allows abstraction; this saves a fair bit of time esp. when having many refinements/interpolations over very long paths

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14807 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Cleanup cgroups even if sys.exit() is called within benchmark script
(changed copied from VerifierCloud r4123).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14808 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fix script in case creating cgroups failed:
variable cgroups was referenced although not assigned in this case

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14809 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move the calculation which cores should be assigned to the current run
out of the setupCGroups method of runexecutor.py.
This calculation should be done at the beginning of the benchmark
with global knowledge.
Furthermore, this is the main remaining difference of this script
to its VerifierCloud version.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14810 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Simplify the handling of the CPU core limit in the benchmark script.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14811 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move the calculation of the to-be-used CPU cores from runexecutor.py
to localexecution.py.
This makes runexecutor.py more reusable.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14812 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove unused parameter from OOMHandler

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14813 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Pass memory limit as a separate parameter to runexecutor,
and use bytes as unit.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14814 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove script that is not used anymore.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14815 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Pass time limits in runexecutor directly
and not in a dict to make it more explicit.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14816 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove now unused parameter "rlimits" in runexecutor.py.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14817 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Avoid lots of constraints in the SMT formulas
about the address of variables that never have their address taken.
These constraints are only necessary in a specific use case.
We previously added them always because it seemed to increase
performance, but this can no longer be reproduced.
Furthermore, these constraints make the formulas more complex,
hinder debugging and add irrelevant information to produced
counterexamples.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14818 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Eliminate one reason for non-determinism of predicate abstraction:
we collected all new predicates in a ListMultimap
and iterated over the keys, but the Multimap is normally based on a
HashMap.

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