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