Counter-Examples

Overview

The Counter-Examples plug-in aims at providing counter-examples from failed proof attempts by the WP plug-in. More precisely, it generates a test case for the C function under analysis from the model given by the automated theorem prover (currently, only Alt-Ergo is supported).

Usage

Here are a few usage examples of the Counter-Examples plug-in:

frama-c -wp [WP options] -then -ce-unknown

This will generate counter-examples for any annotations marked with Unknown status by WP.

frama-c -eva [Eva options] -then -ce-alarms

This will try to generate a counter-example for each alarm generated by Eva. Note, however, that in the absence of additional annotations, such as function contracts and loop invariants, the context in which the counter-example is searched for will be too broad, and the generated counter-examples might be irrelevant.

Other options are listed in the README.md and via the command-line option -ce-help.

Counter-Examples also includes some GUI features, such as popup menu entries and a panel listing all generated counter-examples, with highlighting features.

Technical Notes

• Since the logical theories in which WP’s proof obligations are expressed are undecidable, the logical model might be only partial. Namely, provers aim at being correct (when they answer that the property is true, this is always the case), and the price to pay is incompleteness (when they give a model that might falsify the property, the model might be spurious).

• The Counter-Examples plug-in itself is not always able to take into account all the information provided by the prover, which make the counter-example generated at the C level less conmplete.

Dependencies

Counter-Examples depends mainly on results of the WP plug-in. A few options depend on Eva.

Contact

The plug-in is currently available under a proprietary licence. For any questions, remarks or suggestions, please contact Virgile Prevosto.