CPROVER Eclipse Plugin

About this Plugin

The CPROVER Eclipse plugin is an extension of the Eclipse framework with support for the CPROVER Model Checker suite, including CBMC. The plugin is suitable for Windows, Linux and MacOS.

Installation Instructions

  1. Download and install Eclipse CDT Luna.

  2. Download and install CBMC 5.0 or newer.

  3. Open Eclipse.
    Windows only: you have to run Eclipse from the Visual Studio Command Prompt. We recommend you install the free Visual Studio Community. If you run Eclipse directly, preprocessing will fail!

  4. Select Help → Install New Software... → Add...

  5. Enter a name for the update site (e.g. "CPROVER Plugin") and enter the URL http://www.cprover.org/eclipse-plugin/.

    Click "OK".

  6. Select "CBMC" for installation and click "Next".

  7. Click "Finish".

Usage

  1. Open a C/C++ project.

  2. Create a CBMC run configuration by selecting the menu Run → External Tools → External Tools Configurations.

    • Select CBMC on the left-hand side and create a new run-configuration for your project by clicking on the leftmost icon (document+).
    • Enter a name for the run configuration (e.g. CBMC_configuration) and select the CBMC executable in your file system (Browse...). Then you have to select the source files to be analysed. There are three possibilities:
      1. In order to check all source files in the project, select a project via "Projects..."
      2. In order to check a single source file in your project, choose one via "Source Files..."
      3. Furthermore, it possible to analyse files that have been pre-compiled using the goto-cc tool. Select "goto-cc File..." for that purpose.

    • Press Apply to save the CBMC Run configuration.

  3. Press Run to start CBMC. The results are given in the "CBMC" tab.

  4. If a property check fails, the property is marked with a white/blue cross. We can now examine the reason of failure by debugging the counterexample trace. This is done by selecting Debug from the context menu (right click) of the failed property.

  5. The counterexample debugger uses the standard Eclipse Debug perspective and behaves very similar to a normal debugger. One can step through the program and examine the values of the variables.