The data member and the write_* methods of sharing_node_innert and
sharing_node_leaft are made protected and existing external callers are
refactored to not use write_* directly.
This adds a reset() method which clears the contents of the shared pointer.
Furthermore, the code to remove a reference to the pointed-to object is factored
out into a method destruct(). The method is used both by the destructor and by
reset().
Applying CBMC on large code bases
requires sometimes to model a test environment.
Running a program until a certain point and let it
crash, allows to analyze the memory state at this point in time.
In continuation, the memory state might be reconstructed as base for
the test environment model.
By using gdb to analyze the core dump, I don't have to take
care of reading and interpreting the core dump myself.
When passing `assume(symbol == constant)` or `if symbol == constant then GOTO`, we can populate the
constant propagator and value-set accordingly and use that information until the next merge point without
that constraint. We implement this by allocating and defining a fresh L2 generation on this path, which
will be merged as "real", assignment-derived generations are. Symbols are subject to propagation under
the same conditions as they are on assignment (e.g. requiring that they are not subject to concurrent
modification by other threads).
The previous set-up failed to compile (as cudd.h was not found), and
first fixes to make it compile and link resulted in persistent
segmentation faults. These were caused by inconsistent includes as
HAVE_CUDD was only set in selected directories (unlike the CMake
configuration).
Instead the result of from_exprt and the input of as_expr should be
BDDs.
This makes it possible to reuse the same manager for several exprt
conversion and to combine the results obtain from the from_expr
conversion with BDD operations.
There should only be a single place to hold type information, including
attributes, to ensure consistency. Future changes will remove the "type" member
of goto_functiont, making the type information stored in the symbol table the
single, authoritative source of information.
With this commit the information will remain available in both places, but all
read accesses only use the information in the symbol table.
Removed previously disabled checks:
Not every instruction has a code member - so removed checks that both
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil
sourcelocation as this would have to be optional (if enabled fails
many regression tests). This also simplifies considerably the overall
validation pass (removes much passing around of the options structure).
Removes check on function return type - this will be preserved (#4266)
goto_model::validate now has default parameters.
Minor fixes.
Removed previously disabled checks:
Not every instruction has a code member - so removed checks that both
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil
sourcelocation as this would have to be optional (if enabled fails
many regression tests). This also simplifies considerably the overall
validation pass (removes much passing around of the options structure).
Removes check on function return type - this will be preserved (#4266)
goto_model::validate now has default parameters.
Minor fixes.
There are several checks, implemented with separate methods, and
some flagged as optional.
NB use of validate_goto_model(*this, vm) in goto_functions.h is to avoid
circular inclusion as function_mapt is a nested type and so cannot be
forward declared.
byte_update lowering now proceeds as follows:
1) Determine the size of the update, with the size of the object to be
updated as an upper bound. We fail if neither can be determined.
2) Turn the update value into a byte array of the size determined above.
3) If the offset is not constant, turn the object into a byte array, and
use a "with" expression to encode the update; else update the values in
place.
4) Construct a new object.
source_location.h is transitivly included in almost every translation unit.
Avoid the prefix.h include by moving the a method definition to the cpp file.
xbauch