--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example and automatic provers



-- Julien Signoles (2017-07-18)
> Actually, the WP plug-in has a dedicated Alt-Ergo output, while it relies on Why3 for the other provers. It may explain Jens's results.


Since Why3 has a translation to Alt-Ergo as well, it would be easy to check, by using this path with Alt-Ergo on a run.
--
Yannick Moy, Senior Software Engineer, AdaCore




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170718/83609479/attachment.html>