Consider the following unlikely sequence of events:
$ cat ~/tmp/can-delete/main.c
int main (int argc, char **argv) {
return 0;
}
$ goto-cc main.c -o main.goto
$ cbmc main.goto --function main
CBMC version 5.11 (cbmc-5.11-881-gd52cd0d1e-dirty) 64-bit x86_64 linux
Reading GOTO program from file
Reading: /home/martin/tmp/can-delete/main.goto
failed to insert argc symbol
SUPPORT FUNCTION GENERATION ERROR
argc and argv both exist and it is fine to re-use them. If the
addition fails it will throw an exception, the .second bool is only
false in the case they already exist which is likely harmless.
Now that we have a single-argument constructor for dereference_exprt
there isn't any need to pass the type in to checked_dereference. It
is a potential source of bugs that we might use the followed type and
therefore use a struct type instead of a struct tag-type, which will
cause type consistency problems elsewhere.
Check that the type of the operand is a pointer type and the type of the
dereference expression is precisely the subtype. This should catch any
mistakes where we have followed a struct-tag type to get a struct type,
which will mess up our strict requirements for type equality.
A temporary variable should be created for the `this` argument of a
virtual function call when there is a dispatch table and the `this`
argument involves a dereference.
Copy directly preceding ASSUMEs, changing the argument for `this` to
the new temporary variable for `this`. This is mainly aimed at null
checks, to make the local safe pointer analysis work. We stop as
soon as we find an instruction that is not an ASSERT or ASSUME.
This means that merge_goto's special merge logic for generation zero works on both dead local variables
and on #return_value global variables defined for the second and subsequent times, discounting the
control-flow where the variable is dead.
The string solver was consuming a very large amount of memory with the limit set to 10000;
this appears to be pure chance whether the solver picks a solution requiring universals to be
instantiated a large number of times. The other tests in this directory are already set to
limit string length to 1000, so I just do the same thing here.
Removing this doesn't appear to have any bad consequence, and line numbers cannot generally be relied upon,
since compiling with -g:none or stripping all debug info means they won't be available.
Add a variant of the multianewarray test to check this works, and expand it slightly with comment-out parts
that presumably at some point did not work, but do now.
This is possible now that #return_value variables are not subject to special rules
in phi_function, and the value-set is cleared when variables are marked dead, meaning
that there is no chance a second function call which only sometimes defines #return_value
might witness the previous call's results.
Now that the front-ends are required to explicitly assign a nondet value where that
is intended (e.g. an undefined extern global), rather than leaving an undefined value,
there is no need to special-case merging them.
This saves memory while achieving very similar behaviour as a read from a value removed from
the value-set still yields a failed object. The difference is what happens on a merge:
a merge with an explicit failed object retains it, while a merge against an empty value-set
will discard the undefined possibility. This is fine for dead variables, where on a control-
flow convergance we may safely assume we came from the path where it is not dead, but for
declarations and undefined extern variables the front-end and goto-symex must collaborate to
ensure an explicit nondet value is present.
This enables us to distinguish the case where the front-end intended a nondet
initialiser from an undefined variable, such as a "#return_value" global before
a call or on paths which throw an exception.
Michael Tautschnig