Skip to content

Latest commit

 

History

History
69 lines (49 loc) · 2.67 KB

installation.md

File metadata and controls

69 lines (49 loc) · 2.67 KB

CPROVER Manual TOC

Installation

Requirements

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.

  1. Linux: the preprocessor and the header files typically come with a package called gcc, which must be installed prior to the installation of CBMC.

  2. Windows: The Windows version of CBMC requires the preprocessor cl.exe, which is part of Microsoft Visual Studio. We recommend the free Visual Studio Community.

  3. MacOS: Install the XCode Command Line Utilities prior to installing CBMC. Just installing XCode alone is not enough.

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.

Installing the CBMC Binaries

  1. Download CBMC for your operating system. The binaries are available from http://www.cprover.org/cbmc/.
  2. Unzip/untar the archive into a directory of your choice. We recommend you add this directory to your PATH environment variable.

You are now ready to use CBMC. We recommend you follow the tutorial.

Building CBMC from Source

See the CPROVER Developer Documentation.

Installing the Eclipse Plugin

Requirements

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.

Installing the Eclipse Plugin

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.