The comment calling `java_record_outputs` was uncertain about what it
was doing. The implementation of `java_record_outputs` is now split into
3 functions in order to make it clearer exactly what things are marked
as outputs. The type signature has been updated to return a
`code_blockt` in order to avoid returning the results by output
parameter.
Using it->code.set(ID_statement, ...) no longer suffices as it will not set
code.id(), which is ID_nil after initialisation. Thus any such instruction is
removed during goto-program cleanup.
Use the recently added APIs instead, which will ensure proper initialisation.
For some reason we had not included these in our standard set of regression
tests, and sure enough they got out of sync and one actual regression happened.
remove_returnst::do_function_calls may introduce new instructions. Doing so
requires a call to compute_location_numbers to ensure instruction numbers are
assigned. To avoid recomputing location numbers across all goto functions, the
facility from goto_functionst is used, which will ensure globally unique
location numbers (though they might not be globally contiguous).
This reverts commit abbb389422.
In #2089 a broad cleanup of redundant calls to .update() was done. Let's stay in
this spirit and call .update() when necessary, and not "just to be safe."
To create docker file, run "make" in integration/xen. The Docker file will
build CBMC, download Xen upstream version, and one-line-scan, and then attempt
to build Xen using goto-cc.
The man page states: "In general, whenever a condition wait returns, the thread
has to re-evaluate the predicate associated with the condition wait to determine
whether it can safely proceed, should wait again, or should declare a timeout. A
return from the wait does not imply that the associated predicate is either true
or false."
The regression test is based on
pthread-divine/condvar_spurious_wakeup_false-unreach-call.c from SV-COMP.
In goto-harness:
- we used is_static && is_lvalue to determine something was global.
Turns out that this also applies to extern functions for some reason,
so we ended up accidentally creating nondet assignments to those.
We now check type.id() != ID_code as well.
- we declared pointers to local variables. In if blocks. Which went
out of scope before using them. This meant we had a bunch of
dangling references. We solve this by creating global variables
for our pointer-pointees instead of local ones.
Co-authored-by: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Co-authored-by: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Benchmarks not including headers files fail as we only provided a definition of
__builtin_alloca, which alloca expands to in standard libary headers, but none
for alloca directly.
The example arguments file is named with _example suffix like the existing example method list,
and the branch and develop CSV files are so named and listed in (x, y) order everywhere.
In some places the non const version of .type() and others would be
called.
We force the const version to be called by using as_const.
In the example in
`jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5`
this reduced the number of calls to detach from 744638 to 736844.
This is useful in particular when we want to force the const version of
a method to be called.
For exprt there can be differences in performance between const and
non-const.
There are several reasons why we should not maintain this here:
* We do not have a single use in the code base.
* It's completely unrelated to program analysis or any other CBMC matter.
* If anyone else uses it, they are more than welcome to copy the implementation.
* It was based on MIT-licensed code copyrighted by an external author. Mixing
licenses within individual files is questionable practice.
We already tried to ignore org.cprover.CProver methods such as nondetInt, relying upon
the front-end to supply stub bodies if desired based on their type. However, by creating
symbols for them as for normal (non-stub) methods, but then refusing to provide a body or
advertise them as normal methods, we failed to set up their type properly (specifically
the parameter names), as they were neither set like a stub (upon symbol creation, upon
discovery by a caller) or like a normal method (during java_bytecode_convert_method). By
refusing to create the symbol at all, this treats the special CProver methods more like
normal stubs: their symbols are now created on demand.
It is also no longer necessary for java_bytecode_languaget::methods_provided to special
case them, as they are not added to method_bytecodet either, again matching "real" stub
methods more closely.
Thomas Spriggs