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] New Frama-C version: Fluorine

Hi Francois,

as said Romain, thanks for the release !

I have something for you!

I tried to build a minimal example but I don't know if I succeed.
The issue seem to lie in the axiomatic encoding of definitions in the why3 backe
nd.

Here is the code 

/*@ axiomatic def { 
  @   type hidden_t; 
  @   logic hidden_t injection (real x);
  @   logic hidden_t X = injection(-0.05); 
  @   predicate good(hidden_t x); }
*/

//@ ensures (good(X));
void inst2(float x) {
}

$ frama-c -wp -wp-prover why3:Alt-Ergo -wp-out v3 code_v3.c
gives
--- Why3 (stderr) :
------------------------------------------------------------
File "v3/typed/A_def.why", line 17, characters 42-45:
Unbound symbol 'prefix -..'
------------------------------------------------------------

If you look at generated files:

$ more v3/typed/Axiomatic.why 
function l_X : a_hidden_t = (l_injection (-..05e0))

The previous example where you change -0.05 in 0.0( works like a charm.

Thanks 

pl

	Subject: Re: [Frama-c-discuss] New Frama-C version: Fluorine
	Date: Tue, Apr 23, 2013 at 02:28:26PM +0200

Quoting Fran?ois Bobot (francois.bobot at cea.fr):
> On 23/04/2013 11:33, Jobredeaux, Romain J wrote:
> >Thank you for the new version!
> 
> Thank you for spotting this error.
> 
> >------------------------------------------------------------
> >File "toto2/typed/A_lists.why", line 12, characters 5-11:
> >syntax error
> >------------------------------------------------------------
> >[wp] [Alt-ergo] Goal typed_inst2_post : Failed
> >      Error: Why3 exits with status [1]
> >
> 
> Some names where not uncapitalized in the why3 output.
> This small patch should fix that:
> 
> 
> diff --git a/src/wp/ProverWhy3.ml b/src/wp/ProverWhy3.ml
> index 8e6d990..64fea28 100644
> --- a/src/wp/ProverWhy3.ml
> +++ b/src/wp/ProverWhy3.ml
> @@ -70,8 +70,8 @@ let engine =
>    let module E = Qed.Export_why3.Make(Lang.F) in
>  object(self)
>    inherit E.engine
> -  method datatype = ADT.id
> -  method field = Field.id
> +  method datatype x = self#basename (ADT.id x)
> +  method field x = self#basename (Field.id x)
>    method link e f =
>      match Lang.link e f with
>        | Engine.F_call   s ->
> 
> 
> Thanks,
> 
> -- 
> Fran?ois
> 
> _______________________________________________
> 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
> 

-- 
Pierre-Lo?c Garoche
Research Scientist @ ONERA
pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130423/8baad3e8/attachment.pgp>