Includes a basic Statement List language interface (although without any
typechecking yet) as well as modifications to some Makefiles and
cbmc_languages.cpp. Use the --show-parse-tree option when parsing a .awl file
to see the project's output.
We were doing this in multiple places, this should make it a bit easier to keep
set properties consistent among different places.
Ideally we could eventually move away from mentioning targets from modules here
on the top level (and instead have each module call cprover_default_properties)
but this isn't done in this commit.
Because memory analyzer depends on GDB being present and further uses platform
specific functionality at the moment it had some ifdef functionality to disable
itself.
This made the code a bit more complicated than it needed to be, and also lead to
the code effectively building defunct executables. This removes these ifdefs and
instead excludes memory-analyzer (and related tests) from the build unless
requested (via WITH_MEMORY_ANALYZER environment variable or CMake option
depending on whether it is a Make or CMake build respectively).
Also force building memory-analyzer on Linux and test it there by
default (unless explicitly unset). Behaviour on other platforms should be
preserved.
Right now we have the `goto-cc` tool to create goto binaries from C
files and link goto binaries together. This adds a similar type of
"linker" tool for the symtab language.
I had considered extending 'goto-cc' to handle symtab files as well,
however goto-cc (quite reasonably) makes some C-specific assumptions
about its input files, and I'd figured rather than working around that
it'd be easier to just have a simple command line tool to invoke
`goto_convert` and `link_goto_model` (which, in the end, is all we want
to do for json_symtabs).
This is now consistent with the warnings that Visual Studio would generate,
which warns about missing enum cases in switch/case even when a default: is
present.
This makes Cudd be configured and build at the configuration phase. This
simplifies a bit the logic for dependencies of cudd and cudd-cplusplus
targets.
This is the only way I found to make Ninja build flawlessly.
This commit adds an option to CMake, `WITH_JBMC`, that controls whether
the jbmc directory will be built. It is switched on by default,
preserving the current behaviour.
The motivation is to make it as easy as possible for users to get
started with CBMC, especially users who are only interested in the C
front-end and are on Windows, where installing the JDK and Maven is a
painful exercise.
Also updated `COMPILING.md` to note that you can pass `-DWITH_JBMC=OFF`
to cmake to avoid building jbmc.
Just like is done for Release builds, NDEBUG shouldn't be set for RelWithDebInfo
builds either. Although we are trying to move away from straight "assert" and
use invariants instead, we a) haven't completed this yet and b) imported code
such as optional.hpp continues to use "assert."
This adds a new executable called goto-harness. Right now it doesn't actually do
anything, but ultimately its purpose will be to generate "harness" functions for
goto-programs - i.e. given some specification, it'll generate a function
suitable as a cbmc entry point function that implements that specification.
Planned for now are two types of harnesses: One that takes the name of a
function with parameters and then generates a function that sets up these
parameters and calls the function with them. This is similar to what cbmc does
already, however will allow more flexibility in choosing how exactly these
parameters will be initialised which was deemed out of scope for cbmc. The other
will be able to take a snapshot of a concrete execution of a program, and then
start an analysis from that point.
Implement JSON symtab language, a new, more generic
language frontend, able to read GOTO programs in JSON
form, from any frontend that generates them. Currently
this stands as the support frontend for our ADA
conversion tool, GNAT2GOTO.
Also fixes a number of shortcomings of the earlier approach as far as CMake is
concerned:
- Adds --dirty to the git command line (as is done for Makefiles).
- Does not require a rebuild when there are no changes to the version string.
- CBMC release number updates will be reflected and trigger a rebuild (even when
no other changes have taken place).
This uses the output of `git-describe --tags --always --dirty` to create a UID
for binaries. This includes last tag, number of commits after last tag,
shortened SHA1 checksum and optional dirty flag for uncommited changes. In case
of tagged commit, only the tag name is used.
Lukasz A.J. Wrona