--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on April 2013 ---
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>