Adds support for the conversion of boolean expressions. Note that this
will hardly have any effect on the output of CBMC and in the current
state only be used by projects which rely on it.
There are several STL-specific simplification routines integrated in the
conversion, e.g. changing the conversion order of operands to avoid
unnecessary nesting.
The test in this commit checks for a bug in which the initial nondet
assignment to struct fields was missing from --trace (always showing
these struct fields as being initialised to 0).
Before we simply took the first instruction with the line number geq to the one
specified. Now we go through all instructions and take the one closest.
These used to have side-effects on their parameters, and will still compile if used that
way, so let's use NODISCARD to enforce that their new return value is consulted when
necessary.
When string refinement was walking a tree it broke all sharing as it
went due to requesting a non-constant iterable which makes copies of all
elements within it before returning. This causes memory problems
depending upon size of expressions that are then created - more
complicated the program and string expressions, the worse this got.
The error message used to be
failed to load class 'Test'
This commit makes it
failed to load class Test
The reasoning is that there is no need to quote the class name, it is
totally clear where it starts and where it ends.
Replace it with '. For example, This changes an error message from
failed to load class `java.nio.file.Path'
to
failed to load class 'java.nio.file.Path'
The reason is that the convention of using ` for opening single
quotes looks odd in most modern fonts. For more discussion please
read:
https://www.cl.cam.ac.uk/~mgk25/ucs/quotes.html
By requiring the user to provide the type we can get byte count from
the provided type, not as an argument, which allowed size to be
incorrectly specified
This means that any member-of-symbol constructs introduced by a nested dereference,
such as x->y ==> (x == &o1 ? o1 : o2).y, can be simplified to produce e.g.
(x == &o1 ? o1.y : o2.y) ==> (x == &o1 ? o1..y : o2..y). value_set_dereferencet will
then special-case the if-expression, dereferencing the inner o1..y and o2..y individually.
In the best case where each has a single possible alias, &o3 and &o4 respectively, we
end up with (x == &o1 ? &o3 : &o4), rather than the current result:
let p = (x == &o1 ? o1 : o2).y in (p == &o3 ? o3 : o4)
This was already happening in most cases (e.g. symex_dereference would apply field-sensitivity
before symex_assign_rec was entered), but the case of a statically non-constant but dynamically
constant array index or byte-extract offset would only be handled *after* symex_assign_rec, leading
to an asymmetry in which operations were combined into the ssa_exprt and which ones accumulated in
the expr_skeletont.
With this change the LHS expression is maximally renamed and simplified before symex_assign_rec is
entered, which means that any field-sensitive symbols on the LHS are fully constructed as early as
possible, and expr_skeletont only accumulates those member, index and byte-extract operations which
*cannot* be associated with an ssa_exprt. This means there is no need to undo with-operations or
try to simplify byte-extract operations in goto_symext::assign_from_non_struct_symbol, as this has
been taken care of already, and the l2_full_lhs can be constructed from the expression skeleton
trivially.
This renames the rvalue components of an lvalue expression to L2, such as the index of an array
expression or the offset involved in byte-extract operation. Lvalue components (e.g. symbols) are
left alone.
Matthias Weiss