CProver manual
|
CBMC is available for Windows, i86 Linux, and MacOS X. CBMC requires a code pre-processing environment comprising of a suitable preprocessor and an a set of header files.
cl.exe
, which is part of Microsoft Visual Studio. We recommend the free Visual Studio Community.Important note for Windows users: Visual Studio’s cl.exe
relies on a complex set of environment variables to identify the target architecture and the directories that contain the header files. You must run CBMC from within the Visual Studio Command Prompt.
Note that the distribution files for the Eclipse plugin include the CBMC executable. Therefore, if you intend to run CBMC exclusively within Eclipse, you can skip the installation of the CBMC executable. However, you still have to install the compiler environment as described above.
PATH
environment variable.You are now ready to use CBMC. We recommend you follow the tutorial.
See the CPROVER Developer Documentation.
We provide a graphical user interface to CBMC which is realized as a plugin to the Eclipse framework. Eclipse is available at http://www.eclipse.org. Installation is very simple. Just download the latest version and extract the files.
Important note for Windows users: Visual Studio’s cl.exe
relies on a complex set of environment variables to identify the target architecture and the directories that contain the header files. You must run Eclipse from within the Visual Studio Command Prompt.
The installation instructions for the Eclipse Plugin, including the link to the download site, are available here. This includes a short tutorial on the Eclipse plugin.
Last modified: 2024-11-12 09:30:37 +0200