Adds ACSL importer

_fc-plugins/acsl-importer.md

+---
+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