User Tools

Site Tools


how_do_i

How Do I ... ?

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.

Contribute to CBMC via github

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:

Do once:

  1. Set up a github account
  2. Click fork in the upper right-hand corner of https://github.com/diffblue/cbmc
  3. git clone your newly created fork into a local directory of your choice

For all future improvements, bugfixes, etc:

  1. Create a new branch in your repository
  2. Make your edits, until you arrive at a clean commit/series of commits.
  3. Push your branch to github (that's your own repository)
  4. Point your browser to https://github.com/diffblue/cbmc and you'll immediately be asked whether you want to create a pull request.
  5. Click “compare across forks” in order to select your own fork.

Building

Use an alternative SAT solver?

  1. Download the source of the solver
  2. Edit the config.inc file to give the location of the SAT solver.
  3. Edit “solvers/sat/satcheck.h” to pick the correct solver. In the case of solvers that have similar files / a common heritage, it may be necessary to comment out the other solvers or build conflicts may be caused. MiniSAT 2 and Glucose definitely have this problem.
  4. Build.

For example for Glucose, do the following:

1. In CBMC's src directory, run:
make glucose-download

2. Edit the config.inc file:
#MINISAT2 = ../../minisat-2.2.1
GLUCOSE = ../../glucose-syrup

3. Edit the solvers/sat/satcheck.h file:
//#define SATCHECK_MINISAT2
#define SATCHECK_GLUCOSE

4. Run:
make

Preprocessing

How do I skip the preprocessor?

If the file is name .i then the preprocessor will be skipped; much like most C Compilers.

Usage

How do I analyse Windows code on a Linux machine?

The --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.

Internals

Are objects of type ''dt'' immutable

If 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:

  1. Call write on an irept and save the reference.
  2. Copy the irept.
  3. Modify the original via the reference.

This will also change the copied irept as they both refer to the same dt object. Avoid writing code that does this!

I want to transform the goto-program generated from the input C file before the model-checker is invoked.

In, '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.

How do I add a command line option to CBMC?

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 flows from cmdline to bmct::options. 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_bool_option(const std::string&), optionst::get_int_option(const std::string&) and optionst::get_option(const std::string&) respectively. Since optionst is a map from string to 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.

Once bmct::options is populated, it can be accessed through out the lifespan of bmc.

Modelling

Are arbitrary length bit-vectors available ?

Yes; see The Manual, especially __CPROVER_bitvector.

How do I declare thread local variables?

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 ansi-c directory:

extern _Thread_local unsigned long __CPROVER_thread_id;

NB: This isn't actually CPROVER specific syntax, but properly part of the C11 standard.

Windows

Why do I need the ''cl.exe'' binary on Windows? (Or: how to avoid it.)

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.

I've just updated and now nothing will compile

With Visual Studio it is necessary to run make clean after any changes to the code.

How Do I Set up a Visual Studio Project File for CBMC et al.

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 generate_vcxproj.

  1. Open a bash shell, e.g., provided by cygwin
  1. do cd scripts and then ./generate_vcxproj

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.

how_do_i.txt · Last modified: 2016/05/03 11:30 by schram