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.

  • Subject: [Frama-c-discuss] Tutorial ACSL By Example + WP plugin.
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Tue, 18 Oct 2011 11:50:46 +0200
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