For use in a downstream repository. This is used to indicate whether a
method was synthesized by the java compiler, as opposed to being a
method which has corresponding user written java code.
The message handler field was owned by the classes inheriting from
parse_options_baset which lead to strange patterns where the handler
reference was initialized using a reference to a field which was not
constructed yet.
This is cleaner and avoid some reference duplications.
This does not save many lines of code, but the way we access arrays
using pointer arithmetic can be a bit confusing and it makes sense to
abstract it away and keep the documentation of why we do things this way
in one place.
Character.toChars was malformed (it tried to address a java::array[char] * like it was
a raw char[], and tried to return an if_exprt of two arrays of differing type), and there
is already an implementation in the models library with a perfectly good implementation.
Character.highSurrogate and lowSurrogate were type unsound (creating additions of mixed type).
Again, they add nothing on top of the shipped models library.
Struct member and array index expressions are replaced by new SSA
symbols such that updates to individual fields of structs or arrays do
not affect the SSA index of the remaining object. This enables more
fine-grained constant propagation, which should be particularly
beneficial to Java (where structs/classes prevail).
I came across a few places where the single-parameter constructor was
not used yet and the information about the type of the expression was
duplicated, so I tidied up all occurrences of this that I could find.
Previously when dealing with multidimensional arrays we could end up generating expressions
such as array[idx] = ALLOCATE Something; array[idx]->field1 = x; array[idx]->field2 = y;
This was a struggle for symex, as every reference to array[idx] could be a bad dereference,
and so symex::invalid_object (or perhaps some_symbol$object) references were created to account
for this possiblity. By using a temporary (generating code like
`t = ALLOCATE Something; t->field1 = x; t->field2 = y; array[idx] = t;`) it is much clearer
that the pointer dereferences must refer to the newly allocated object, and so the problematic
case is avoided.
This simplifies the preprocessing and leave it to the model to handle
the complexity, which is less error-prone (writing safe java program is
easier than write c++ that generates safe goto-program).
Update the models for a version of getClass which uses
CProver.classIdentifier.
This is necessary for getting rid of the preprocessing of getClass which
is error-prone.
https://github.com/diffblue/java-models-library/pull/21
thomasspriggs