This is a hack, but "__asm__ __volatile__ ("mfence": : :"memory");" doesn't compile on windows and the way CBMC handles "__asm mfence" needs to be fixed. Currently "__asm mfence" is not recognised as a function by CBMC.
For the call graph, we add the function to the call graph but do not try to look for function calls in the body.
For slicing global inits, we do not try to look in the function body for symbols.
This fixes issue https://github.com/diffblue/cbmc/issues/2631
In particular, goto_check did not properly handle pointers whose value was an
integer address (such as int *p = 0x10 in the test case memory_allocation1).
This commit adds in pointer checks on pointers which are integer addresses,
treating them essentially the same as pointers which are unknown (and could
therefore point to any of the more well-defined types of memory objects),
except that they are known not to be null, so no check for NULL is needed.
Previously the SSA trace did all concretisation (taking the solver's output
and turning it into concrete expressions to be output in the result trace) before
sorting the steps by time and determining what belongs in the final trace. This
was generally harmless, but could result in much wasted time and potentially
memory exhaustion when concretising very large arrays and strings.
Therefore, we now perform the time-order sort and figure out which steps are
to be kept first, *then* concretise them.
This currently breaks an assertion as described in the .desc file. It should be re-enabled
once string-refinement knows how to introduce sufficient indirection to overcome this.
The local-safe-pointers analysis can already inform symex that certain pointers
are known not to be null at particular program points. This strengthens the analysis
to spot more cases such that it can determine no null pointer is dereferenced in the
new regression test `jbmc/clean_derefs`, which exercises many common Java operations
including array accesses.
The specific improvements to local-safe-pointers:
* Look through typecasts. This was already done for GOTO instructions, but now works
for ASSUME as well.
* Search for not-null expressions using base_type_eq instead of just irept::operator<.
This means that when symex uses namespacet::follow to remove a symbol_typet that does
not prevent local-safe-pointers from noting it is not null in a particular context.
Daniel Poetzl