Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Tutorial ACSL By Example + WP plugin.

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