Skip to content
Snippets Groups Projects
Commit e80b5ad4 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Adds ACSL importer

parent 3aabac47
No related branches found
No related tags found
1 merge request!47Adds ACSL importer
Pipeline #28499 passed
---
layout: plugin
title: ACSL Importer
description: Import ACSL specifications from extern files
key: specifications
distrib_mode: proprietary
---
## Overview
This plug-in adds to Frama-C support for out of C source files ACSL specification. Therefore
it 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.
In addition, the plug-in allows to enter ACSL annotations directly via the Graphical User
Interface.
## Usage
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.
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
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment