--- layout: fc_discuss_archives title: Message 58 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



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