--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on February 2014 ---
-- 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