|
Eclipse Plugin for CBMC
Requirements:
- Windows: You need Visual Studio (as preprocessor). The Visual Studio
executables need to be in the PATH environment
variable.
- Linux: You need
gcc and the usual header files.
To download and install the Eclipse plugin for CBMC, do the following:
- Install Eclipse, version
3.2. You must install it into some location that
does not contain spaces in the path
name. The plugin does not work with Eclipse version 3.1.
- Start Eclipse, open "Help" → "Software Updades" → "Find and Install"
- Select "Search for new features to install", then "Next"
- Click "New remote site", Name: "CBMC Plugin",
URL Linux:
http://www.verify.ethz.ch/satabs/plugin/lin/
URL Windows:
http://www.verify.ethz.ch/satabs/plugin/win/
URL Mac OS X:
http://www.verify.ethz.ch/satabs/plugin/osx/
- Select the "CBMC Plugin", klick "Finish"
- Select "org.feature.CProver"
- Read and accept license, then "Finish"
To use the plugin:
- Click "New" → "Project" → "CProver" → "New
Verification Project"
- Select the new project
- Clock "New" → "New Task"
- Double-click the task
- "Files" tab: choose the files to model check
- "Options" tab: various options for running CBMC/Satabs
- Create a new CPROVER launch configuration using the green run button.
- After running CBMC, the claims for the selected task
are displayed in the "Claims" view.
- Click on "Check All" in the "Claims" view to run the model
checker
- If a counterexample is produced for a claim, click on the claim
to step through the trace.
|