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] Type casts and wp
- Subject: [Frama-c-discuss] Type casts and wp
- From: jaseg at physik.tu-berlin.de (Sebastian Götte)
- Date: Fri, 24 Aug 2018 21:55:13 +0200
Hi, I'm a grad student of computer science currently playing around with frama-c in their spare time and I've struck one case where I don't understand the behavior of frama-c/wp. Given the following program frama-c/wp cannot prove the assert c_gt_0. Everything else is proven successfully. Intuitively it seems to me that from x >= 0 and x != 0 follows x > 0, and indeed for d that is the case, but not for c. I would like to understand why that is so. $ cat narf.c #include <unistd.h> /*@ @ requires 0 <= d < 256; @*/ size_t test(char foo, unsigned int d) { unsigned int c = (unsigned char)foo; if (c != 0) { //@ assert c_lt_256: c < 256; //@ assert c_ge_0: c >= 0; //@ assert c_ne_0: c != 0; //@ assert _0_le_c: 0 <= c; //@ assert c_gt_0: c > 0; return c + d; } if (d != 0) { //@ assert d_lt_256: d < 256; //@ assert d_ge_0: d >= 0; //@ assert d_ne_0: d != 0; //@ assert d_gt_0: d > 0; return c + d; } return 23; } void main(void) { test(23, 42); } $ frama-c -wp -wp-rte narf.c > [kernel] Parsing narf.c (with preprocessing) > [rte] annotating function main > [rte] annotating function test > [wp] 10 goals scheduled > [wp] [Alt-Ergo] Goal typed_test_assert_c_gt_0 : Unknown (Qed:7ms) (56ms) > [wp] Proved goals: 9 / 10 > Qed: 8 (0.48ms-2ms-12ms) > Alt-Ergo: 1 (9ms) (14) (unknown: 1) $ frama-c --version > Chlorine-20180502 Thank you for any input, Sebastian
- Follow-Ups:
- [Frama-c-discuss] Type casts and wp
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Type casts and wp
- Prev by Date: [Frama-c-discuss] Chlorine configure error: Unbound value Z.numbits
- Next by Date: [Frama-c-discuss] Type casts and wp
- Previous by thread: [Frama-c-discuss] Chlorine configure error: Unbound value Z.numbits
- Next by thread: [Frama-c-discuss] Type casts and wp
- Index(es):