--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on October 2011 ---
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