--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Puzzled about apparent proof of false contract



Hi there.

My students were quite happy when they succeeded in proving with Frama-C
that one of their programs satisfied the contract they believed was the
right one.  However, they discovered that Frama-C proves the ensures
clause also with a too-weak requires clause that, because of unsigned
overflows, makes the contract false for (at least) one input value.

The program is attached: it was analyzed with Neon on a 64-bit Ubuntu 14.04
machine.  We used Alt-Ergo and we have both "RTE" and "Invariants" selected.
All the balls apart from the one on the requires clause come out green.
On the "Console" tab we have:

[kernel] preprocessing with "gcc -C -E -I.  sum.c"
[rte] annotating function sum
[wp] Collecting axiomatic usage
sum.c:15:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 7 goals scheduled
[wp] Proved goals:    0 / 7
[wp] [Qed] Goal typed_sum_assert_rte_unsigned_overflow : Valid (1ms)
[wp] [Qed] Goal typed_sum_assert_rte_unsigned_overflow_3 : Valid (1ms)
[wp] [Alt-Ergo] Goal typed_sum_assert_rte_unsigned_overflow_2 : Valid (Qed:1ms) (27ms) (5)
[wp] [Alt-Ergo] Goal typed_sum_post : Valid (Qed:3ms) (86ms) (19)
[wp] [Qed] Goal typed_sum_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_sum_loop_term_decrease : Valid (22ms) (10)
[wp] [Alt-Ergo] Goal typed_sum_inv : Valid (Qed:1ms) (910ms) (8)

We are puzzled: what are we missing?
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com
-------------- next part --------------
#include <assert.h>

/*
  requires n <= 92681;
  ensures \result == (n*(n + 1))/2;
*/

/*@
  requires n <= 92682;
  ensures \result == (n*(n + 1))/2;
*/
unsigned int sum(unsigned int n) {
  unsigned int ris;
  /*@ loop variant n; */
  for (ris = 0U; n > 0U; --n) {
    /* This assertion would fail:
       assert((((unsigned long long)ris) + n) > 4294967295ULL); */
    ris += n;
    /*@ invariant ris+(n*(n-1)/2) == \at(n,Pre)*(\at(n,Pre)+1)/2; */
  }
  return ris;
}

int main() {
  unsigned int n = 92682U;
  unsigned int r = sum(n);
  unsigned long long rl = r;
  unsigned long long nl = n;
  assert(rl == (nl*(nl + 1))/2);
  return 0;
}