This is intended to be a quick question and answer page. Post questions you'd like answers to or snippets of information that fits this format.
Once CBMC has fully moved to github, the preferred way of contributing improvements and bugfixes is via pull requests. While you may find information on how to do this on various web tutorials, it's actually very easy:
For all future improvements, bugfixes, etc:
config.incfile to give the location of the SAT solver.
For example for Glucose, do the following:
1. In CBMC's src directory, run:
2. Edit the
#MINISAT2 = ../../minisat-2.2.1
GLUCOSE = ../../glucose-syrup
3. Edit the
If the file is name
.i then the preprocessor will be skipped; much like most C Compilers.
--win32 option will over-ride the auto-detection of platform specific behaviour and make
cbmc behave as if it was run on a Windows machine.
SHARING is not defined (is by default) then no; every
irept has it's own instance of
dt and these are mutable. If
SHARING is defined then probably. 'write()' causes a shallow copy of the
dt object. It is possible to hold on to the reference provided by write (for example, via a function parameter) and make multiple modifications on the same write, giving a mutable
dt object. This is done infrequently in the code. Note that this can also create problems if you:
ireptand save the reference.
This will also change the copied
irept as they both refer to the same
dt object. Avoid writing code that does this!
'src/cbmc/parseoptions.cpp there is a method called
cbmc_parseoptionst::doit(). This method calls
cbmc_parseoptionst::get_goto_program(options,bmc,goto_functions). After the call returns
goto_functions contains the goto-program corresponding to the input C file.
goto_functions can be transformed at this point. Information on how to modify goto-programs can be found here.
Let's say you want to add an option called
–hypothetical-option to CBMC. In file,
src/cbmc/parseoptions.h you will see a macro named
CBMC_OPTIONS. If you want to add a short option (the option does not need an argument) then you need to add another line to the macro
“(hypothetical-option)”. If you need to add a long option (option that takes an argument) then you need to add a colon
“(hypothetical-option):”. These options will be available through a data-structure of type
cmdlinet. One can query whether a particular option was provided using
cmdline.isset(“hypothetical-option”) which returns true/false. The value/argument provided to the option can be retrieved through
cmdline.getval(“hypothetical-option”) which returns a
const char *.
In CBMC these command line options are further stored in
bmct::options (data structure of type
optionst). One can refer to
cbmc_parseoptionst::get_command_line_options(optionst&) where information
optionst has a map of type
map<std::string,std::string>. Setting an option with a boolean value is done through
optionst::set_option(const std::string&,const bool). Similar variants exist for setting an option with int or string values. Retrieval is done through
optionst::get_int_option(const std::string&) and
optionst::get_option(const std::string&) respectively. Since
optionst is a map from
string it does internal conversion while retrieving an option as integer or bool. Using
get_option() on an option with a boolean value may have undesired effect/error/exception. Therefore, the correct method must be call for each type.
bmct::options is populated, it can be accessed through out the lifespan of
Yes; see The Manual, especially
Thread local variables can be declared by providing a type specifier
_Thread_local. Here is an example from the
pthread_lib.cpp file in the
extern _Thread_local unsigned long __CPROVER_thread_id;
NB: This isn't actually CPROVER specific syntax, but properly part of the C11 standard.
CProver uses the platform's native C preprocessor. On Windows, this defaults to Visual Studio's CL command. On Unix-style platforms (including Linux and OS X) the default is to use GCC. To support cygwin-like environments, the
--gcc command line parameter was added, which enforces the use of GCC as preprocessor.
With Visual Studio it is necessary to run
make clean after any changes to the code.
Daniel says : In order to reduce the amount of work required to set up a Visual Studio project file for CBMC and the associated tools, we have created a script that automates this process.
The script is available in the CBMC SVN trunk in the directory
scripts and is called
cd scriptsand then
This reads the Makefiles and automatically generates project files for cbmc, goto-cc and goto-instrument, which you can open in Visual Studio. The project files come with filter definitions that order the source files according to the (top-level) subdirectory they are in.
Note that the flex and bison tools and the irep_id conversion tool still need to be run manually.