The makefile was pointing at the wrong directory, which somehow didn't
cause a CI failure, this corrects that. In doing so realised that the
test was slightly inaccurate, so resolved this issue as well.
symex and goto-analyze (through the goto_modelt class) now support
setting the --function flag on precompiled .gb files.
Refactored out the function flag and its help function to
rebuild_goto_start_functions.
Used this extracted flag in goto-analyze, symex and CBMC.
Added tests that check both goto-analyze and symex when ran with the
--function flag actually generate the correct _start function. Also
added tests for when it isn't a precompiled binary. Added these new
folders to the overal test suite
Invariant in `uncaught_exceptions_analysist::output` expects all
functions in the GOTO model to be present in the exceptions_map.
However, functions like __CPROVER_assert(...) get replaced by explicit
GOTO instructions and will not occur as function calls, thus not be in
the map. This fix addresses this issue, which only occurs in a debug
output produced with -DDEBUG.
Previously the zombie child would continue on the same code path as the forking
parent. Hence one would see spurious "Remove failed" message as the zombie
child would try to perform the same file removal as the parent.
goto-gcc now runs the ls_parse.py script whenever the target codebase is
being compiled with a custom linker script (specified with the -T
option). goto-gcc then synthesizes the linker script definitions that
ls_parse reported, and adds them to the goto-program as if those
definitions were defined in the target C program rather than the linker
script.
This solves a problem where the values of some C variables are
inaccessible from CBMC because those variables are defined in the linker
script rather than the C codebase. It also solves the problem of CBMC
not knowing what memory regions are accessible to the C program, again
because the memory regions are declared to be valid in the linker
script.
This commit also introduces three tests for this functionality.
This commit also fixes a small bug in ls_parse.py that made it reject
some valid linker scripts.
Input programs containing __CPROVER_assume, __CPROVER_assert etc. can
now be compiled with goto-gcc as well as goto-cc. Previously, the
system compiler would complain about missing function bodies for all of
these CPROVER macros.
Packed unions/structs without alignment specification may use fields of
dynamic size. It is then unnecessary to compute their full size as it
would never be used anyway.
dump-c previously would not print __CPROVER__start code as this is deemed
tool-internal. With increasing support for test-harness construction, the
harness code may be of interest to users, who may wish to tweak and use re-use
it.
Cbmc can potentialy run out of memory if no maximum string length is
set. This happens more often with the new version of check axioms
because a concretization step is made to be more precise in the check.
Daniel Kroening