--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VC not the same when verifying function in isolation or in complete compilation unit



Hi,

To be able to use Alt-Ergo 1.01 with Frama-C Magnesium, a solution would be
to have a wrapper that calls Alt-Ergo with option "-backward-compat" 
enabled.

Regards,
Mohamed.

--
Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.info
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979




Le 08/04/2016 16:01, Christophe Garion a écrit :
> I have written something wrong in my previous mail: all my proof
> attempts have been done through Why3 (I have upgraded my
> installation of Alt-Ergo to version 1.01 and Frama-C Magnesium cannot
> parse Alt-Ergo 1.01 outputs).