--- layout: fc_discuss_archives title: Message 127 from Frama-C-discuss on November 2013 ---
27/11/2013 14:20, David MENTRE wrote: > Hello, > > 2013/11/27 BAUDIN Patrick <Patrick.Baudin at cea.fr>: >> The ACSL importer plug-in (used to import external ACSL file) takes care of >> that situation. >> Unfortunately, this plugin isn't free. > Even if this plug-in is not available, how one would use this plug-in > to solve this issue? > As you will see, it is easy to use: it automatically does the transformation. ACSL specification are allowed in C files, but aren't mandatory. Here, I removed all ACSL specifcation from your C files and just created this file: > cat q18.acsl function g: contract : requires p <= 10; ensures \result == p + 1; assigns a; function incr_a: contract : requires a <= 10; ensures a == \old(a) + 1; assigns a; function f: contract : assigns a; Then the following command gives : > frama-c q18_a.c q18_b.c -acsl-import q18.acsl -print [kernel] preprocessing with "gcc -C -E -I. q18_a.c" [kernel] preprocessing with "gcc -C -E -I. q18_b.c" [acsl-importer] Success for q18.acsl [acsl-importer] Done: 1 file. /* Generated by Frama-C */ int f(int p); static int a = 0; /*@ requires a ? 10; ensures a ? \old(a)+1; assigns a; */ void incr_a(void) { a ++; return; } /*@ requires p ? 10; ensures \result ? \old(p)+1; assigns a; */ int f(int p) { int __retres; if (a <= 10) incr_a(); __retres = p + 1; return __retres; } /*@ requires p ? 10; ensures \result ? \old(p)+1; assigns a; */ int g(int p) { int tmp; tmp = f(p); return tmp; }