fixed a bug in the LiveVariables class, while checking whether a variable is live or not, only variables in the same function should be taken into account

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14458 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Complete rewrite of the LiveVariablesTransferrelation plus the necessary changes in the other files.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14459 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Updates to the rationals implementation.
More performant and more consistent version.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14461 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Update Google AppEngine SDK

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14462 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
removed configuration for log level and output

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14463 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed incorrect ("overoptimized") implementation of #addEssentialFields() in PTS

  for nested structures there were no way to start tracking for any inner structure field if the
  structure always occurred as inner (see comment in the method).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14464 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added test case for the inner structure field tracking bug (in prev. commit)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14465 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed issue #182 arising due to deferred allocaion (void *) pointer shifting

  e.g. void *a = malloc(); a += (unsigned long)n;
  // see, for instance, function pdc20621_put_to_dimm, called from pdc20621_dimm_init in Linux 3.17, SATA SX4 driver

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14466 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New maximization interface for Z3:

more general with more features.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14468 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
trivial refactorings: inline simple method

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14469 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
refactoring: make some inner classes static,
and reduce visibility of modifying methods

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14470 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move static utility method from VariableClassification
into the class where it belongs.
VariableClassification is not the place for utility methods
used by other classes.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14471 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move lots of code for creating the VariableClassification
into a separate builder class.
Make all collections in VariableClassification immutable,
they are handed out to callers all the time.

With this change,
the VariableClassification is not created lazily anymore.
Most analyses need it anyway, so we do normally do not save time on lazy
creation.
Lazy creation complicates things, for example exceptions are not handled
properly currently, and the timing statistics of CFA creation
do not contain the time for creating the VariableClassification.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14472 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Proper exception in VariableClassificationBuilder:
do not wrap expected checked exceptions in AssertionError.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14473 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Do not store Dependencies object in VariableClassification anymore.
It is mutable but we want immutable data,
and it stores more than we need.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14474 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Move class Dependencies from VariableClassification
to VariableClassificationBuilder,
it is used only there.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14475 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improve API:
use several methods with clear names
instead of an int parameter with special values like -1

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14477 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Make some sets in VariableClassificationBuilder
local variables instead of fields,
because they are needed only at one point in time
and not for the full time of the building process.

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