Search code examples
cvisual-studiocbmc

CBMC as standalone?


is it possible to run CBMC as stand alone witout Visual Express ? Do I need to recompile it or is there another trick maybe ?

I only need to use CBMC to translate a function to CNF regularly, so I want to call it with the function name, write the cnf file to disk and start again. I do not want to use Visual Studio.


Solution

  • It is entirely possible to run The CBMC model checker as a standalone program. I do it weekly on both Linux and Windows 7 :)

    I'm assuming you're on Windows because of Visual Studio.

    Open a command prompt and navigate to the folder where cbmc.exe is, and call it like so: cbmc --help ...to see the options you have.

    The user manual has a section on how to do it, in 3.2 Command line interface. You may have to call the batch-script that sets up Visual Studio's environment for the CLI (VSVARS32.bat / vsvarsall.bat etc). On some Windows machines, that script is placed in c:\program files\microsoft visual studio\[version]\vc\bin\ if I recall correctly.

    See this MSDN page for more info on that: https://msdn.microsoft.com/en-us/library/f2ccy3wt.aspx