Commit e5154847 authored by François Bobot's avatar François Bobot
Browse files

Add Farith as "plugins"

parent 895c2501
Pipeline #36983 failed with stage
in 9 minutes and 4 seconds
- name: About
link: /html/overview.html
id: overview
- name: Features
link: /html/kernel-plugin.html
id : features
- name: Documentation
link: /html/documentation.html
id : documentation
......
---
layout: plugin
title: ACSL Importer
description: Import ACSL specifications from extern files
key: specifications
distrib_mode: proprietary
---
## Overview
The plug-in allows to import external ACSL specifications written in files,
separated from the C source files.
That provides more flexibility in the use of ACSL in the life cycle of
software since the merge between the specifications and the source code is
done by the plug-in.
In addition, the plug-in allows to enter ACSL annotations directly via the Graphical User
Interface.
Therefore `ACSL Importer` plug-in is useful only to people that intend to write
ACSL specifications and do not want to write them inside comments of the C source files.
## Usage
The use of the plug-in could be the following, except if the given options lead
to run analysis (analysis should be launched through the graphical interface):
- `frama-c-gui <importing options> <C files>`
Otherwise, options have to be splitted into two groups and given as follow:
- `frama-c-gui <importing options> <C files> -then <analysis options>`
Once the plugin installed, the next command gives the up-to-date list of the
plug-in options:
- `frama-c -acsl-importer-help`
All options of the plug-in are prefixed by `-acsl-`.
The main options are:
- `-acsl-importer-help`:
lists all options specific to the plug-in
- `-acsl-import <filename list>`:
analyzes the content of files listed in its arguments and inserts the correctly typed
specifications in the abstract syntax tree of Frama-C for further processing.
- `-acsl-Idir <dirname list>`:
specifies the list of directories where the relative file names mentioned in include
directives are searched.
- `-acsl-keep-unsed-symbols`:
configures Frama-C kernel such that unused C symbols aren't removed before the import.
- `-acsl-parse-only`:
parses the ACSL files without typing nor imports.
- `-acsl-typing-only`:
parses and types the ACSL files without imports.
- `-acsl-version`:
pretty prints a text containing the version ID of the plugin.
## Example
The plug-in can be used as follows. From a C file:
```c
int f ( int i );
int g ( int j );
void job ( int *t , int A) {
for ( int i = 0; i < 50; i ++) t[i] = f (i );
for ( int j = A; j < 100; j ++) t[j ] = g(j );
}
```
and a specification file:
```
function f:
contract:
ensures P(phi(C(\result)));
assigns \nothing ;
function g:
contract: assigns \nothing ;
function job:
at 1: assert 50 <= A <= 100;
at loop 1:
loop invariant 0 <= i <= 50;
loop invariant \forall integer k; 0 <= k < i == > P(t[k]);
loop assigns i,t[0..49];
at loop body 1:
contract:
ensures i == \old(i);
at loop stmt 1:
contract:
requires i==0;
ensures i==50;
at loop 2:
loop invariant A <= j <= 100;
loop assigns j,t[A ..99];
at return:
assert \forall integer k; 0 <= k < 50 == > P(t[k]);
at call f:
contract:
ensures P(phi(C(t[i])));
```
The following command line:
```
frama-c -acsl-import demo.acsl demo.c -print -no-unicode
```
generates the following output:
```
# frama-c -acsl-import demo.acsl demo.c -print -no-unicode
[kernel] Parsing demo.c (with preprocessing)
[acsl-importer] Success for demo.acsl
[acsl-importer] Done: 1 file.
[kernel] Parsing demo.c (with preprocessing)
[acsl-importer] Success for demo.acsl
[acsl-importer] Done: 1 file.
/* Generated by Frama-C */
/*@
axiomatic A {
type event = B | C(integer);
predicate P(integer x) ;
logic integer phi(event e) ;
}
*/
/*@ ensures P(phi(C(\result)));
assigns \nothing; */
int f(int i);
/*@ assigns \nothing; */
int g(int j);
void job(int *t, int A) {
/*@ assert 50 <= A <= 100; */
{
int i = 0;
/*@ requires i == 0;
ensures i == 50; */
/*@ loop invariant 0 <= i <= 50;
loop invariant \forall integer k; 0 <= k < i ==> P(*(t + k));
loop assigns i, *(t + (0 .. 49));
*/
while (i < 50) {
/*@ ensures i == \old(i); */
{
/*@ ensures P(phi(C(*(t + i)))); */
*(t + i) = f(i);
}
i ++;
}
}
{
int j = A;
/*@ loop invariant A <= j <= 100;
loop assigns j, *(t + (A .. 99)); */
while (j < 100) {
{
*(t + j) = g(j);
}
j ++;
}
}
/*@ assert \forall integer k; 0 <= k < 50 ==> P(*(t + k)); */
return;
}
int T[100];
void main(void) {
job(T,50);
return;
}
```
## Contact
The plug-in is currently available under a proprietary licence.
For any questions, remarks or suggestions, please contact
[Patrick Baudin](mailto:patrick.baudin@cea.fr?subject=[ACSL Importer]).
---
layout: plugin
title: Aoraï
description: Verify specifications expressed as LTL (Linear Temporal Logic) formulas.
key: specifications
distrib_mode: main
manual_pdf: /download/frama-c-aorai-manual.pdf
---
## Overview
The **Aoraï** plug-in provides a method to automatically annotate a C program
according to an LTL formula *F* such that, if the annotations are verified,
then we ensure that the program respects *F*.
The classical method to validate annotations is to use the [Wp](wp.html) or
[Eva](eva.html) plug-ins.
## Installation Dependencies
Aoraï is available in the main Frama-C distribution. It used to be
available from http://amazones.gforge.inria.fr/aorai, but the version
currently hosted there is obsolete and won't compile with newer versions of
Frama-C.
If you want to use LTL syntax for properties, you have to install the
[ltl2ba](http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php) tool in your
path. This tool is distributed by its author, Paul Gastin (ENS Cachan),
under the GPL licence and converts an LTL formula into a Büchi automaton.
## Usage
The plug-in is activated with one of the following command lines:
frama-c file.c -aorai-ltl file.ltl
frama-c file.c -aorai-automata file.ya
These two commands differ only by the syntax used to express the
property to be verified: *.ltl* files are described in an ltl-like syntax,
while *.ya* are description of automata in an yacc-like syntax.
Options are:
- `-aorai-verbose`:
Gives some information during computation, such as used/produced files
and heuristics applied.
- `-aorai-show-op-spec`:
Displays, at the end of the process, the computed specification
of each operation, in terms of Büchi states and transitions.
- `-aorai-dot`:
Generates a dot file of the Büchi automaton. Dot is a graph
format used by the [GraphViz](http://www.graphviz.org) tool.
- `-aorai-acceptance`:
If set, considers acceptation states (Only on finite traces).
If not, only the safety is verified.
- `-aorai-output-c-file`: *file*
Outputs the annotated program in *file* (the default is to
derive a name from the one of the first input file).
- `-aorai-help`:
Gives the whole list of options.
## Installation Dependencies
- Only the safety part of properties is checked. The liveness part is not truly
considered. Currently, a liveness property is only a restriction that the
terminating state of the program has to be an accepting state.
Hence, if the program terminates, then the liveness property is verified.
- Currently, function pointers are not supported.
- In the init state from the automaton, conditions on C arrays and C structures
are not statically evaluated (which would be an optimization)
but are supported.
## Contact
Aoraï has been originally written by
[Nicolas Stouls](mailto:nicolas.stouls@insa-lyon.fr?subject=[Plug-in Aorai]),
[CITI Labs](http://www.citi-lab.fr), [AMAZONES team](http://amazones.gforge.inria.fr).
It is currently maintained by CEA LIST as part of the main Frama-C distribution.
See our [contact](contact.html) page for more information.
**End Note:** to the question "*Why this name: Aoraï?*" my answer is: why not?
Aoraï is the name of the tallest reachable mount in the Tahiti island and its
reachability is not always obvious.
## Further Reading
- [Short documentation]({{page.manual_pdf}})
- [A few simple examples](/download/frama-c-aorai-example.tgz)
Other resources can be found at
[the official web page of Aoraï](http://amazones.gforge.inria.fr/aorai/).
---
layout: plugin
title: CaFE
description: Verification of CaRet temporal logic properties
key: specifications
distrib_mode: free
repo_url: https://github.com/Stevendeo/CaFE
---
## Overview
CaFE (CaRet Frama-C Extension) is a small model-checker dedicated
to prove CaRet properties over C programs.
[CaRet](https://doi.org/10.1007/978-3-540-24730-2_35) is
"a temporal logic of nested calls and returns", i.e. a flavor of
temporal logic well suited to describe a program's call stack.
## Usage
[CaFE]({{page.repo_url}}) is available as a
separate open-source plug-in. Once installed, it will be activated by
the `-cafe` option, while `-cafe-formula` allows specifying
the file in which to formula to be verified lies. A typical command will
thus be the following:
frama-c -cafe file.c -cafe-formula file.caret
## Dependencies
CaFE uses [Eva](eva.html) internally to compute an over-approximation
of the states of the program.
---
layout: plugin
title: Conc2seq
description: Verification of concurrent programs
key: concurrent
distrib_mode: free
repo_url: https://github.com/AllanBlanchard/Frama-C-Conc2Seq
---
## Overview
Conc2seq is dedicated to the verification of concurrent C programs.
More specifically, it proposes an instrumentation of the original code
that simulates all possible interleavings allowed by the C standard.
The resulting instrumented code is then a sequential program that can be
analyzed as such. Note however that the transformation assumes that the
original code is sequentially consistent, which must be verified independently
(e.g. by using the [Mthread plugin](mthread.html)).
## Usage
Conc2Seq is available as an external open-source [plug-in]({{page.repo_url}}).
Once installed, it is enabled with the `-c2s` option, which will generate a
sequential version of the concurrent API implementation provided to Frama-C.
The generated code and specification is available a new project.
To output this simulating program into a file, use the option
`-c2s-output filename`.
---
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]).
---
layout: plugin
title: E-ACSL
description: Runtime Verification Tool.
key: main
priority: 1
manual_pdf: /download/e-acsl/e-acsl-manual.pdf
additional:
- name: "E-ACSL language reference manual"
short: "Language reference"
link: /download/e-acsl/e-acsl.pdf
- name: "E-ACSL language reference implementation manual"
short: "Language implementation"
name_for_main_dl: "E-ACSL implementation"
link: /download/e-acsl/e-acsl-implementation.pdf
distrib_mode: main
---
## Overview
Frama-C's **E-ACSL** plug-in automatically translates an annotated C program
into another program that detects the violated annotations at runtime.
If no annotation is violated, the behavior of the new program is the same as
the one of the original program.
Combined with other Frama-C plug-ins that generate annotations, the
verification process is pretty automatic and may verify much more properties
than standard testing. This way, it is a
[memory debugger](https://en.wikipedia.org/wiki/Memory_debugger)
offering functionalities comparable to Valgrind and AddressSanitizer,
and even more powerful.
More precisely, possible usages include:
- detection of a large class of undefined behaviors (in conjunction
with the [RTE](rte.html) plug-in);
- verification of high-level properties (in conjunction for
instance with the [Aoraï](aorai.html) or [SecureFlow](secureflow.html)
plug-ins);
- complementing static and dynamic analyses (i.e. trying to
find test cases that trigger alarms generated by [Eva](eva.html) or act
as counter-examples for annotations marked as unknown by [WP](wp.html)),
in conjunction with the [StaDy](stady.html) plug-in;
- debugging specifications, in conjunction with a test-case generator such as
[PathCrawler](pathcrawler.html) or [AFL](http://lcamtuf.coredump.cx/afl)
## Quick Start
E-ACSL comes with a convenient script *e-acsl-gcc.sh* which may be called
as follows:
e-acsl-gcc.sh -c <files>
It generates three files, `./a.out`, `./a.out.frama-c` and `./a.out.e-acsl`.
The first one is the binary produced by `gcc` from the input files;
the second one is the instrumented file with the monitor generated by E-ACSL
from the input files. The third one is the binary produced by `gcc` from this
latter file, so monitoring the annotations.
Its execution behaves in the same way as the two other files, except that it
fails if an annotation is violated.
In order to automatically check that no **undefined behaviors** of many kinds
are executed, the script can be simply used as follows:
e-acsl-gcc.sh -c --rte=all <files>
## Dependencies
The **E-ACSL** plug-in can use the results of both [RTE](rte.html) and
[Eva](eva.html) plug-ins. It can be combined with several other plug-ins,
such as [WP](wp.html), [Aoraï](aorai.html), [SecureFlow](secureflow.html),
[StaDy](stady.html), [PathCrawler](pathcrawler.html), [MetACSL](metacsl.html), etc.
## Further Reading
- [E-ACSL user manual]({{page.manual_pdf}})
{% for add in page.additional %}
- [{{add.name}}]({{add.link}}){% endfor %}
---
layout: plugin
title: Eva, an Evolved Value Analysis
short: Eva
description: Automatically computes variation domains for the variables of the program.
key: main
distrib_mode: main
priority: 0
manual_pdf: /download/frama-c-eva-manual.pdf
---
## Value analysis based on abstract interpretation
The **Evolved Value Analysis** plug-in computes variation domains for variables.
It is quite automatic, although the user may guide the analysis in places.
It handles a wide spectrum of C constructs.
This plug-in uses abstract interpretation techniques.
<img src="/assets/img/plugins/eva-img.png">
The results of **Eva** can be exploited directly in two ways:
- They can be used to infer the absence of run-time errors.
The results are displayed in reverse, that is, alarms are emitted for all
the operations that could lead to a run-time error. If an alarm is not
emitted for an operation in the source code, then this operation is
guaranteed not to cause a run-time error.
- The Frama-C graphical user interface displays the inferred sets of possible
values for each variable, in each point of the analyzed program.
## Quick Start
The plug-in can be used both with the graphical user interface and in batch
mode (recommended). In batch mode, the command line may look like:
frama-c -eva file1.c file2.c
A list of alarms (corresponding to possible run-time errors as computed by the
analysis) is produced on the standard output.
The results of **Eva** are used by many other plug-ins. In this case,
the analysis is initiated automatically by the exploiting plug-in, but it is
still possible to configure it for the case at hand (e.g. through the same
command-line options that would be used in conjunction with `‑eva`.
## First Example
Consider the following function, in file `test.c`:
```c
int abs(int x) {
if (x < 0) return -x;
else return x;
}
```
In this code, Eva reports the possible integer overflow when `x` is the
smallest negative integer by emitting an alarm at line 2.
The alarm is the [ACSL](/html/acsl.html) assertion `assert -x ≤ 2147483647;`
that protects against an overflow.
**Eva** also displays the possible values of the variables at the end of the
function. Here, we can see that the result is always positive.
```
$ frama-c -eva test.c -main abs
[…]
mytests/test.c:2:[eva] warning: signed overflow. assert -x ≤ 2147483647;
[eva] done for function abs
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function abs:
__retres ∈ [0..2147483647]
```
One can also inspect in the graphical interface of Frama-C the alarms emitted
by Eva, as well as the possible values inferred at each program point.
## Technical Notes
- Maturity: industrialized.
- Recursive calls are currently not supported.
- Only sequential code can be analyzed at this time.
## Further Reading
The options to configure the analysis as well as the syntax of the results are
described in the [Eva user manual]({{page.manual_pdf}}).
---
layout: plugin
title: Farith, proved library for FloatingPoint computation
short: Farith
description:
key: main
distrib_mode: main
priority: 0
manual_pdf: /download/farith-manual.pdf
manual_html: /html/doc/farith/coq/index.html
---
## Farith
[Coq documentation]({{page.manual_html}}).
---
layout: plugin
title: Frama-Clang
description: C++ front-end to Frama-C, based on the clang compiler.
key: front
distrib_mode: free
manual_pdf: /download/frama-clang-manual.pdf
---
![Frama-Clang logo](/assets/img/plugins/frama-clang.png)
## Overview
Frama-Clang is a plugin that allows Frama-C to take as input C++ programs.
As its name implies, it is based on the [clang](http://clang.llvm.org)
compiler, the C/C++/Objective-C front-end of the [llvm](http://llvm.org)
platform. More precisely, Frama-Clang is composed of two parts: a clang plugin
(written in C++) that produces a simplified version of the clang AST, and a
normal Frama-C plugin that takes as input this simplified version and produces
a normal Frama-C AST.
When this plug-in is in use, Frama-C will consider all files ending in `.cpp`,
`.c++`, `.C`, `.cxx`, `.cc` and `.ii` (considered as already pre-processed)
as C++ files and give them to Frama-Clang to translate them into Frama-C's
internal representation (i.e. a plain C AST).
Once this has been done, any existing analyses can be launched as usual.
**Caveat:** Frama-Clang is currently in an early stage of development.
It is known to be incomplete and comes without any bug-freeness guarantees.
Moreover, the translation from C++ to C does not make any attempts to optimize
the resulting code for the back-end analyzers such as [Eva](eva.html) or