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] Puzzled about apparent proof of false contract

  • Subject: [Frama-c-discuss] Puzzled about apparent proof of false contract
  • From: bagnara at cs.unipr.it (Roberto Bagnara)
  • Date: Tue, 20 May 2014 11:43:32 +0200
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;
}