--- layout: fc_discuss_archives title: Message 1 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 Inconsistent assumptions



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)

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