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

[Frama-c-discuss] WP (v == INT32_MIN) causing "Have: 0 < 0."?



Another issue seems to arise when processing the same code when using 
"==". See the assumed "Have: 0 < 0." and "Prove: false." in the last few 
lines of output below.

- Barrie

$ cat my_abs.c
#include <stdint.h>

/*@
     behavior neg_in_range:
         assumes INT32_MIN < v < 0;
         ensures \result == -v;
*/
int32_t my_abs(int32_t v)
{
   if (v >= 0)
     return v;

   if (v == INT32_MIN)
     return INT32_MAX;

   return -v;
}
$ frama-c -pp-annot -wp -wp-rte -no-unicode -wp-print -wp-proof-trace 
-wp-prover alt-ergo my_abs.c
[kernel] preprocessing with "gcc -C -E -I.  -dD my_abs.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function my_abs
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_my_abs_neg_in_range_post : Valid (4ms)
File "/tmp/wp6d11e6.dir/typed/my_abs_neg_in_range_post_Alt-Ergo.mlw", 
line 104, characters 1-38:Valid (0.0040) (0)
Proof:
    0 > 0

[wp] [Alt-Ergo] Goal typed_my_abs_assert_rte_signed_overflow : Valid 
(8ms) (4)
File 
"/tmp/wp6d11e6.dir/typed/my_abs_assert_rte_signed_overflow_Alt-Ergo.mlw", line 
230, characters 1-148:Valid (0.0080) (4)
Proof:
    -2147483648 <> v_0
    is_sint32(v_0) = true
    -2147483647 > v_0
    -2147483648 <= v_0
   (( -2147483648 <= v_0 /\  v_0 <= (2147483648 - 1)) \/
    is_sint32(v_0) = false)

------------------------------------------------------------
   Function my_abs
------------------------------------------------------------

Goal Assertion 'rte,signed_overflow' (file my_abs.c, line 16):
Assume {
   (* Domain *)
   Type: (is_sint32 v_1).
   (* my_abs.c:10: Else *)
   Have: v_1<0.
   (* my_abs.c:13: Else *)
   Have: -2147483648!=v_1.
}
Prove: -2147483647<=v_1.
Prover Alt-Ergo returns Valid (8ms) (4)

------------------------------------------------------------
------------------------------------------------------------
   Function my_abs with behavior neg_in_range
------------------------------------------------------------

Goal Post-condition for 'neg_in_range' (file my_abs.c, line 6) in 'my_abs':
Assume {
   (* Pre-condition for 'neg_in_range' (file my_abs.c, line 5) in 
'my_abs' *)
   (* Pre-condition for 'neg_in_range': *)
   Have: 0<0.
}
Prove: false.
Prover Alt-Ergo returns Valid (4ms)

------------------------------------------------------------