--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c: WP issues with Alt-Ergo (but works with Z3)



-- Jean-Christophe Filliatre (2014-02-19)
> 
> Hi,
> 
> I know this is not your question, but it seems to me that there are a
> few mistakes in your code:
> 
> - first, "\exists i. A ==> B" shoud rather be "\exists i. A && B" (in
> the post and in the loop invariant)

Interestingly, Why3 issues a warning on such constructs:

warning: form "exists, P -> Q" is likely an error (use "not P \/ Q" if not)

We've copied this warning for Ada contracts in the GNAT compiler:

wrong.ads:3:14: warning: suspicious expression
wrong.ads:3:14: warning: did you mean (for all X => (if P then Q))
wrong.ads:3:14: warning: or (for some X => P and then Q) instead?

Maybe you could have a similar warning in Frama-C.
--
Yannick Moy, Senior Software Engineer, AdaCore