Change handling of constants in PredicateCPA with pointer-alias
handling. Previously, they also got a (dummy) SSA index, now we omit the
index just like we do when pointer-alias handling is enabled.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11308 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
More efficient iteration over sub set of variables.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11309 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move identification of "relevant" variables and fields
from CToFormulaWithUFConverter to CtoFormulaConverter
to prepare for using this option without pointer-alias handling, too.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11310 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Not and Plus is deprecated.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11311 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: We can avoid constructing temporary SMGStates if we shuffle the
moment around, when the stack is dropped and the state is pruned.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11312 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Refactored methods, now we don't need to use different states
when calculating parameter values.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11313 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Fixed Bug, the type of a value can be a typedef.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11314 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Fixed Bug, Method now returns unknown value instead of null.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11315 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removing converter for deprecated UnaryOperations PLUS and NOT. Now the CFA should never contain PLUS and NOT for C-code.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11316 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Rename from ABM to BAM, as discussed

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11317 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
cleanup, removing deprecated code.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11318 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Rename from ABM to BAM, as discussedi; TODO: Rename CPA

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11319 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add a method to clear the entity cache.


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


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11321 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Implemented basic symbolic value formula handling with binary expressions.