CPROVER Eclipse Plugin
About this Plugin
Download and install Eclipse CDT Luna.
Download and install CBMC 5.0 or newer.
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!
Select Help → Install New Software... → Add...
Enter a name for the update site (e.g. "CPROVER Plugin") and enter the URL http://www.cprover.org/eclipse-plugin/.
Select "CBMC" for installation and click "Next".
- Click "Finish".
Open a C/C++ project.
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
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:
- In order to check all source files in the project, select a project via "Projects..."
- In order to check a single source file in your project, choose one via "Source Files..."
- 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.
- Select CBMC on the left-hand side and create a new run-configuration for your project by clicking on the leftmost icon (document+).
Press Run to start CBMC. The results are given in the "CBMC" tab.
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.
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.