Commit 0f2694ca authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'add-counter-examples' into 'master'

add page for counter-examples plugin

See merge request !105
parents 8ab325cc 2b9cadf6
Pipeline #33113 passed with stage
in 1 minute and 28 seconds
---
layout: plugin
title: Counter-Examples
description: Counter-example generation from failed proof attempts
key: specifications
distrib_mode: proprietary
---
## Overview
The **Counter-Examples** plug-in aims at providing counter-examples from failed
proof attempts by the [WP](wp.html) 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](wp.html) plug-in.
A few options depend on [Eva](eva.html).
## Contact
The plug-in is currently available under a proprietary licence.
For any questions, remarks or suggestions, please contact
[Virgile Prevosto](mailto:virgile.prevosto@cea.fr?subject=[Counter-Examples]).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment