--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Type casts and wp



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