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 Inconsistent assumptions

  • Subject: [Frama-c-discuss] WP (v <= INT32_MIN) causing Inconsistent assumptions
  • From: barries at slaysys.com (Barrie Slaymaker)
  • Date: Fri, 02 Aug 2013 11:07:45 -0400
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)

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