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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Mon, 2 Sep 2013 10:59:54 +0200
  • In-reply-to: <51FBCB41.40005@slaysys.com>
  • References: <51FBCB41.40005@slaysys.com>
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