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