The plugin works only within Eclipse 3.2.
If you already installed an old version of the plugin that has the old name (i.e. CbmcSatabs), please uninstall it.
The supported verifiers are: SATABS, CBMC, HW-CBMC and EBMC.
If you intend to use the plugin in Windows OS you first need the MS C++ compiler. It is included in MS Visual C++ Express Edition (download for free from http://msdn.microsoft.com/vstudio/express/visualc/download/). After you install MS Visual C++ Express Edition, you have to append "...\Common7\IDE" and "...\VC\bin" to PATH system variable.
First open the CProver perspective. The CProver perspective contains all the views and menu shortcuts necessary for running the plugin properly.
The plugin also commutes automatically to the CProver perspective whenever you create a new CProver verification project/task or even open a task in the task editor.
Once you are in the CProver perspective, you can very easily create new verification projects/tasks.
A verification project is just a container for verification tasks. It doesn't have any configuration of its own.
Once you have created a verification project, you can create new verification tasks within it.
Once you have created a verification task, the task file (the file that contains all the information about the task) will be opened in the task editor in a very nice and easy-to-use graphical environment, where you can very easily configure the verification task. There are two kinds of tasks: tasks in which you have to manually select the files to be verified, and tasks in which the files to be verified are packed in a goto-program in a form of an xml-binary by 'goto-cc' tool that is shipped with the plugin.
The configuration particularities of the first kind of tasks (that use manual files selection) are:
The configuration particularities of the second kind of tasks (that use a xml-binary) are:
The common configuration issues of a verification task are:
We illustrate some task configurations in the following screenshots:
files selection (manually), files selection (xml-binary), includes / defines, launch options.
Notes:
You can also specify global preferences for the CProver plugin in Windows->Preferences->C-Prover.
The most important are:
The rest are just default values for the launch options of a verification task.
Now you are ready to start a verification session.
To do that, you first need to create a CProver launch configuration, if you haven't created one already.
If you already have one, then just select a task from the project navigator and run it using the CProver launch configuration.
Once you started the verfication session on the selected task, you will quickly get the verification claims in the claims view, in a few seconds, at latest. This operation is performed with versioning on the claim-checking results, i.e. if the old claim-checking results are still valid (task or its files not modified meanwhile) they are shown accordingly.
Before a new verification session is started, the current(running) verification session, if there is one, is automatically stopped. Hence, only one task can be handled by a verification session.
Now, from the claims view, you can perform various operations on the claims or the current verification session.
You can stop, terminate or reset a session from the 'Session' popup menu.
Stopping a session means killing all the running claim-checks, cleaning all the verification views, and hiding all the non-persistent views. The persistent(always visible) views are: the claims view, the claims filter view, the console view and the log view. The rest are all non-persistent, i.e. they are shown only when needed.
Terminating a session is stopping it without the possibility to reset it later on, i.e. the current task is not memorized.
Resetting a session means stopping it and restarting it without versioning , i.e. the existing claim-checking results are discarded, even if they are still valid.
You can check a claim by double-clicking it, or check the selected claims, from the 'Check' popup menu.
You can stop all the claim-checks, or the ones for the selected claims, from the 'Stop' popup menu.
After a claim-check is completed the line coloring of the claim's location is updated accordingly, along with its corresponding status icon. A claim verification can return success , failure (status icon looks like a red X), unknown or error (status icon looks like a red full-circle with a white X inside). It returns error when a parsing error happens, or some binary needed by the chosen verifier is not found. When a claim-check returns failure , it means that a valid(non-spurious) counterexample has been found and its corresponding trace view is immediately shown.
You can navigate through the claims/failures locating at a particular line, within the CProver file editor, by simply clicking repeatedly on the respective line. Also, when you click(select) a claim, its location is shown within the CProver file editor, and also its failure trace, in case there is one (i.e. the claim-check returned failure), is shown in the adequate view. An illustration of these can be seen in the following screenshots: screenshot 1, screenshot 2.
You can easily sort, change the sorting order, or deactivate sorting on some columns by simply clicking on them. All the columns of the claims view, c-trace variables watch view and loops view are sortable.
You can easily filter the claims you wish to see by their status or properties. For instance, if you want to see the claims whose verification return failure or unknwon and whose properties are array bounds or pointer dereference , you just have to check the corresponding nodes in the 'Status' and 'Property' subtrees, as shown in the following screenshot. Therefore, the status filter is in conjunction with the property filter, i.e. they must both hold. Obviously, the status/property filter is a disjunction of options, i.e. reunion of the claims that satisfy the checked status/property nodes. You can also filter the claims by the file in which they reside.
In the loops view you can see the loops of the program. If you click on a loop, its location is show within the CProver file editor. If a loop caused an unwinding assertion failure of some claim-check, then the loop gets a failure status icon (red 'X'). After increasing the bounds of the loops which caused failures because of insufficiently high bounds (bound 0 means 'infinite' bound), you can recheck all the claims whose check returned unwinding assertion failure by clicking the 'Recheck' button.
You can filter the variables you wish to watch in both C trace view and Verilog trace view. See screenshots: screenshot 1, screenshot 2.
When you close Eclipse , the current verification session, if there is one, is stopped automatically.