This avoids having #ifdef SHARING and similar preprocessor instruction
in the middle of the code, and only keep one such #ifdef when irept
chooses to inherit from sharing_treet or non_sharing_treet.
This was obtained by extracting from irept, the part of the code which
would only apply when SHARING is not defined.
This results in a simple self contained class, similar to the
sharing_treet class.
The use of macros in the irept class make its difficult to understand
and prevent to use both possibilities in the same compilation.
This commit extracts from the irept class the part of the code that only
exists when SHARING is defined, which results in a simple, self
contained class.
This replaces preprocessor instructions, making the code a bit clearer
and the node class more reusable.
In particular we can use both the sharing and non sharing implementation
in the same compiled binary. This will be useful when we separate the
sharing and non sharing implementations of irept.
We extract the dt class from irept, rename it to tree_nodet and make
the tree type a template argument.
This exposes more clearly how they depend on each other, and makes it
easier to reason about them independently.
In particular we now see that the node doesn't need to know much about
the tree except that it can be stored in the vector or a map.
We already enforced this when creating a code_returnt, but still permitted
codet(ID_return) that did not have the same. Make sure the C parser always
creates irepts with an operand, and make use of that throughout the code base.
Previously these relied on base_type_eq to hide differently-decorated tags; now they explicitly
just check the tag name, rather than relying on base_type_eq, which will soon go away anyway, to
hide generic qualifiers and/or array element types.
sourcet contains an interator, and the current interface explicitly allows
it to be uninitialised. However, most parts of the code base access
source.pc without checking. This commit removes the option to leave the
source uninitialized.
Avoid doing the same start_function set-up three times, and avoid redundant work
between different initialize* functions when one always calls the other.
sourcet contains an interator, and the interface explicitly allows it to be
uninitialised. However, most parts of the code base access source.pc
without checking.
Avoid the suggestion that `get_static_field` might be expected to create them -- it doesn't,
java_bytecode_convert_class does and we should be able to safely assume they exist
during convert_method.
This avoids multiple lookups in the hash set, each of which requires a number of
operator== and hash() calls. The use of const_cast is acceptable, because we do
not actually change the object in a way that would affect ordering (objects will
continue to have the same hash value and still compare equal).
We furthermore ensure that operator== can use pointer equality when submitting
an already-shared irept to merge_irept. On SV-COMP/ReachSafety-ECA this reduces
the number of recursive operator== invocations from 5,814,764,546 (generated by
4,241,423,614 invocations) to 2,232,563,047 (generated from 4,326,016,698
invocations). That is, despite ~100M additional invocations (because the
performance improvement permits more symbolic execution runs) around 3.6B
recursive calls are avoided.
It's already implicit in a bare pointer (rather than a reference) that it could be null,
so let's just use that to express whether we have an answer or not.
Whether we store the values at ID_C_identifier/ID_C_base_name or elsewhere is an
implementation detail. Includes code cleanup to use a ranged for, and a bugfix
where ID_arguments was still being used when it should be parameters.
Previously if asked to populate a pointer with tagged type (e.g. "Object *") then it would
allocate a "struct Object { ... }", i.e. the struct_typet rather than the struct_tag_typet.
This verifies that it now retains tag types.
The traces need to be correctly truncated so that
the failing property comes last.
The traces are printed in the same order as the properties
are listed in the result report.
This is an implementation for the common idiom in which an existing
instruction is replaced by a skip while retaining the source_location. It
replaces instructiont::make_skip().
Updates to the goto binary version should always be consistent, and shouldn't
require changes in multiple places. Also we never support more than one version
at a time.
Romain Brenguier