--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2013 ---
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) ------------------------------------------------------------