--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2013 ---
I'm trying to learn about Frama-C & co, and have found something that seems like it might be a minor issue in WP. In the below code, using <= as shown causes WP to feed inconsistent assumptions to alt-ergo. Using == doesn't. Frama-C's output is shown below the code, see the "When:" and "Have:" assumptions. If this is an issue with Frama-C (rather than with my understanding), I'll toss it into bts, but I wanted to check here first rather than possibly cluttering bts. - Barrie $ cat my_abs.c #include <stdint.h> /*@ behavior neg_limit: assumes v <= INT32_MIN; ensures \result == INT32_MAX; */ int32_t my_abs(int32_t v) { if (v >= 0) return v; if (v <= INT32_MIN) // Changing "<=" to "==" avoids alt-ergo "Inconsistent assumption" warning return INT32_MAX; return -v; } $ frama-c -version Version: Fluorine-20130601 Compilation date: Thu Aug 1 12:13:03 EDT 2013 Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable) Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable) $ 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] [Qed] Goal typed_my_abs_assert_rte_signed_overflow : Valid [wp] [Alt-Ergo] Goal typed_my_abs_neg_limit_post : Valid (Qed:4ms) (2) File "/tmp/wpebec0b.dir/typed/my_abs_neg_limit_post_Alt-Ergo.mlw", line 230, characters 1-158:File "/tmp/wpebec0b.dir/typed/my_abs_neg_limit_post_Alt-Ergo.mlw", line 230, characters 1-158:Valid (0.0000) (2) Proof: 0 <= my_abs_0 my_abs_0 <= -2147483648 Inconsistent assumption ------------------------------------------------------------ Function my_abs ------------------------------------------------------------ Goal Assertion 'rte,signed_overflow' (file my_abs.c, line 15): Assume { (* Domain *) Type: (is_sint32 v_1). (* my_abs.c:9: Else *) Have: v_1<0. (* my_abs.c:12: Else *) Have: -2147483647<=v_1. } Prove: true. Prover Qed returns Valid ------------------------------------------------------------ ------------------------------------------------------------ Function my_abs with behavior neg_limit ------------------------------------------------------------ Goal Post-condition for 'neg_limit' (file my_abs.c, line 5) in 'my_abs': Assume { (* Domain *) Type: (is_sint32 my_abs_0). (* Residual *) When: 0<=my_abs_0. (* Pre-condition for 'neg_limit' (file my_abs.c, line 4) in 'my_abs' *) (* Pre-condition for 'neg_limit': *) Have: my_abs_0<=-2147483648. } Prove: 2147483647=my_abs_0. Prover Alt-Ergo returns Valid (Qed:4ms) (2) ------------------------------------------------------------