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] 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)

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