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.

Hello Sylvain,

the algorithms and data structures of "ACSL by Example" were verified using
Frama-C/Jessie (Boron and Carbon).

We have evaluated WP and found that roughly half of the examples could also be
directly verified with WP.

Hereby we used the following command line

               frama-c-gui -cpp-command ?gcc -C -E -I.? -pp-annot -wp -wp-proof alt-ergo function_name.c

About 20% of the functions needed some tweaks to get through WP.
The rest (about 36%), we could not verify using WP.
We found that most problems were caused my the way WP currently can (or cannot) handle
axioms with labels and issues concerning memory models.

(As an aside, these numbers refer to a development version of WP that led to the Nitrogen release.
However, we have not yet tried the latest official release.
Note also that we have reported these findings to our colleagues at CEA LIST, as
we are currently in the joint Device-Soft project as part of which  "ACSL by Example" has been produced.)

Regards

Jens

On 18 Oct 2011, at 11:50, sylvain nahas wrote:

Hi,

I am currently following the tutorial "ACSL By Example", but using the
WP plugin.
It does not validate. Is it due to discrepencies between WP and
Jessie, or because the datatypes I have used?

-----------------------------------------------------------------------
frama-c -stop-at-first-alarm -wp -wp-rte -rte-print -wp-warnings
-wp-trace -wp-proof alt-ergo $^ -then -report | tee $@.report
-----------------------------------------------------------------------
/**
* @brief Compares arrays "a" and "b" of size "n"
*/

/** @verbatim */

/*@
predicate is_valid_range(unsigned int *a, unsigned int n) = (n >= 0)
&& \valid_range(a, 0, n-1) ;
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 is_valid_range(a, n) ;
requires is_valid_range(b, n) ;

ensures \result <==> is_equal {Here, Here} (a, n, b) ;
*/
/** @endverbatim */

/** @param[in,out] a First array to compare
* @param[in,out] b Second array to compare
* @param[in] n Size of array
*
* @retval 0 Values in arrays differs (behavior all_equal)
* @retval 1 Arrays contain the same value (behavior some_not_equal)
*/

int equal(const unsigned int *a, unsigned int n, const unsigned int *b){
unsigned int i = 0;
/*@ loop invariant 0 <= i <= n ;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k] ;
loop variant n-i;
*/
for ( i = 0; i<n; i++ )
if (a[i] != b[i])
return 0;
return 1;
}
-----------------------------------------------------------------------
[kernel] preprocessing with "gcc -C -E -I.  equal.o"
[rte] annotating function equal
[wp] [Alt-Ergo] Goal store_equal_loop_inv_1_established : Valid
[wp] [Alt-Ergo] Goal store_equal_assert_6_rte : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_2_established : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_1_preserved : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_2_preserved : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal store_equal_post_1 : Timeout
[wp] [Alt-Ergo] Goal store_equal_assert_5_rte : Timeout
[wp] [Alt-Ergo] Goal store_equal_assert_4_rte : Timeout
/* Generated by Frama-C */
/*@
predicate is_valid_range{L}(unsigned int *a, unsigned int n) = n ? 0 ?
 \valid_range(a,0,n-1);
*/
/*@
predicate is_equal{A, B}(unsigned int *a, unsigned int n, unsigned int *b) =
 ? ? i; 0 ? i ? i < n ? \at(*(a+i),A) ? \at(*(b+i),B);
*/
/*@ requires is_valid_range{Here}(a, n);
   requires is_valid_range{Here}(b, n);
   ensures \result ? 0 ? is_equal{Here, Here}(\old(a), \old(n), \old(b));

*/
int equal(unsigned int const *a, unsigned int n, unsigned int const *b)
{
 int __retres;
 unsigned int i;
 i = (unsigned int)0;
 i = (unsigned int)0;
 /*@ loop invariant 0 ? i ? i ? n;
     loop invariant ? ? k; 0 ? k ? k < i ? *(a+k) ? *(b+k);
     loop variant n-i;
 */
 while (i < n) {
   /*@ assert rte: \valid(a+i); */
   /*@ assert rte: \valid(b+i); */
   if (*(a + i) != *(b + i)) { __retres = 0; goto return_label; }
   /*@ assert rte: i+1U ? 4294967295; */
   i ++;
 }
 __retres = 1;
 return_label: /* internal */
 return (__retres);
}


[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'equal'
--------------------------------------------------------------------------------

[    -    ] Post-condition (file equal.c, line 16)
           tried with WP-Store.
[ Partial ] Loop variant at loop (file equal.c, line 34)
           By WP-Store, with pending:
            - Assertion 'rte' (generated)
            - Assertion 'rte' (generated)
[ Partial ] Invariant (file equal.c, line 30)
           By WP-Store, with pending:
            - Assertion 'rte' (generated)
            - Assertion 'rte' (generated)
[ Partial ] Invariant (file equal.c, line 31)
           By WP-Store, with pending:
            - Assertion 'rte' (generated)
            - Assertion 'rte' (generated)
[    -    ] Assertion 'rte' (generated)
           tried with WP-Store.
[    -    ] Assertion 'rte' (generated)
           tried with WP-Store.
[ Partial ] Assertion 'rte' (generated)
           By WP-Store, with pending:
            - Assertion 'rte' (generated)
            - Assertion 'rte' (generated)
[    -    ] Default behavior
           tried with Frama-C kernel.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
    4 Locally validated
    4 To be validated
    8 Total
--------------------------------------------------------------------------------

BTW, you can see how I managed to let Doygen integrate ACSL spec. into
the function documentation. Less than optimal but does the job.
Maybe one day will be Doxygen able to understand ACSL comments.

Grettings,
Sylvain

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss