From 2b9cadf621bb404cbd7dee7abe443d8c7634d217 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 5 Jan 2021 11:24:52 +0100 Subject: [PATCH] add page for counter-examples plugin --- _fc-plugins/counter-examples.md | 66 +++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 _fc-plugins/counter-examples.md diff --git a/_fc-plugins/counter-examples.md b/_fc-plugins/counter-examples.md new file mode 100644 index 00000000..82014b0f --- /dev/null +++ b/_fc-plugins/counter-examples.md @@ -0,0 +1,66 @@ +--- +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]). -- GitLab