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