# 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; }

**Follow-Ups**:**[Frama-c-discuss] Puzzled about apparent proof of false contract***From:*loic.correnson at cea.fr (CORRENSON Loic 218851)

- Prev by Date:
**[Frama-c-discuss] How to transform a statement with case label by using the visitor?** - Next by Date:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Previous by thread:
**[Frama-c-discuss] How to transform a statement with case label by using the visitor?** - Next by thread:
**[Frama-c-discuss] Puzzled about apparent proof of false contract** - Index(es):