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.

Hi,

Sorry, we are a little busy at CEA this week...
Yes, there are some diff?rencies between WP and Jessie.
In order to get better result with WP, it is adviced of add  "loop 
assigns" clause.
Please refers de ACSL document to find its semantics (Jessy wasn't 
really compliant about it).

You can have a look at this example:

 > cat equals.c
/*@ requires n > 0 ==> \valid(&a[0..n-1]);
     requires n > 0 ==> \valid(&b[0..n-1]);
     ensures n > 0 ==> \result ? 0 ? ? ? k; 0 ? k ? k < n ? a[k] ? b[k];

*/
int equal(unsigned int const *a, unsigned int n, unsigned int const *b)
{
   int __retres;
   unsigned int i;
   i = (unsigned int)0;
   /*@ loop assigns i ;
       loop invariant i1: 0 ? i;
       loop invariant i2: n >= 0 ==> i ? n;
       loop invariant i3: ? ? k; 0 ? k ? k < i ? a[k] ? b[k];
       loop variant n-i;
   */
   while (i < n) {
     if (a[i] != b[i]) {
       return 0;
     }
     i ++;
   }
   return 1;
}
 > frama-c -wp test.c -wp-rte -then -report
[kernel] preprocessing with "gcc -C -E -I.  test.c"
[rte] annotating function equal
[wp] [WP:simplified] Goal store_equal_loop_assigns_2 : Valid
[wp] [WP:simplified] Goal store_equal_loop_inv_1_i1_established : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_1_i1_preserved : Valid
[wp] [Alt-Ergo] Goal store_equal_assert_8_rte : Valid
[wp] [Alt-Ergo] Goal store_equal_assert_7_rte : Valid
[wp] [Alt-Ergo] Goal store_equal_assert_6_rte : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_2_i2_preserved : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_2_i2_established : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_3_i3_preserved : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_inv_3_i3_established : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal store_equal_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal store_equal_post_1 : Valid
[report] Computing properties status...

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

[  Valid  ] Post-condition (file test.c, line 3)
             by WP-Store.
[  Valid  ] Loop assigns (file test.c, line 11)
             by WP-Store.
[  Valid  ] Loop variant at loop (file test.c, line 17)
             by WP-Store.
[  Valid  ] Invariant 'i1' (file test.c, line 12)
             by WP-Store.
[  Valid  ] Invariant 'i2' (file test.c, line 13)
             by WP-Store.
[  Valid  ] Invariant 'i3' (file test.c, line 14)
             by WP-Store.
[  Valid  ] Assertion 'rte' (generated)
             by WP-Store.
[  Valid  ] Assertion 'rte' (generated)
             by WP-Store.
[  Valid  ] Assertion 'rte' (generated)
             by WP-Store.
[  Valid  ] Default behavior
             by Frama-C kernel.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
     10 Completely validated
     10 Total
--------------------------------------------------------------------------------

Kind regards,
Patrick.

Le 18/10/2011 11:50, sylvain nahas a ?crit :
> 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
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin,
CEA, LIST, DILS, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072