--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on September 2013 ---
Thanks for the bug report. We actually corrected some issues on (<=) for the next release. L. Le 2 ao?t 2013 ? 17:07, Barrie Slaymaker <barries at slaysys.com> a ?crit : > 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) > > ------------------------------------------------------------ > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss