--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on October 2011 ---
18/10/2011 13:29, sylvain nahas wrote : > Hi Jens, > > it was very informative, thanks. > > I am at lost now. What should one install to have something working? > Should I fall-back to one of the previous version? But then Jessie is > scheduled for phasing out... > > May somebody from the CEA LIST gives hint? > > Thanks, > Sylvain > Hello, The Tutorial ACSL By Example was built over the capabilities of Jessy. Those of WP plug-in are not the same. For example WP plug-in doesn't infer loop assigns as Jessy does internally. That will be left to another plug-in as run time errors were left to RTE plug-in. Also, some of "loop assigns" of the tutorial are not correct (the variable index is sometimes missing) . It wasn't a real problem for Jessy, because the way Jessy uses them is correct. But with WP plug-in, you have to give correct loop assigns. 18/10/2011 14:25, Pascal Cuoq wrote : > "loop assigns" clauses are also the topic of a series of blog posts: >http://blog.frama-c.com/index.php?tag/ACSL I could understand from your e-mail that nothing is working with WP plug-in. Of course, it isn't the case. Please, look at this example, derived from one of the tutorial: > cat equal.c /*@ predicate is_equal {A,B} (unsigned int *a, unsigned int n, unsigned int *b) = \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B) ; */ /*@ requires n > 0 ==> \valid(&a[0..n-1]) && \valid(&b[0..n-1]); @ ensures \result ? 0 ? is_equal{Here,Here}(a, n, b); */ int equal(unsigned int const *a, unsigned int n, unsigned int const *b) { unsigned int i; /*@ loop assigns i; @ loop variant n-i; */ for (i = 0; i < n; i++) /*@ invariant 0 ? i && is_equal {Here,Here}(a,i,b); */ if (a[i] != b[i]) return 0; return 1; } For my point of you, invariant clauses set on the loop body (also called the "loop invariants ? la CAVEAT" in reference to CAVEAT verification tool from CEA) are more easy to write since execution paths, that don't enter into the loop, have not to be considered. These invariants cut the proof only for executions going into the loop. WP plug-in supports such invariant clauses. The support is experimental (option -wp-invariants) and the behaviour isn't optimal when having several "invariant" clauses or mixing "invariant" and "loop invariant" clauses. > frama-c equal.c -wp -wp-rte -wp-invariants -then -report ... -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- 8 Completely validated 8 Total Kinds regards, Patrick Baudin. -- Patrick Baudin, CEA, LIST, DILS, F-91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072