--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP (v <= INT32_MIN) causing Inconsistent assumptions



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