--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on June 2012 ---
Hello Boris, You do not say which provers you tried... I tried your code with Frama-C Nitrogen + Jessie 2.30 + Why3 0.72 (just with frama-c -jessie <file.c>) and I am able to prove every VCs using Alt-Ergo/CVC3 and or /Z3. I attached the HTML report produced using why3session. Hope this helps, - Claude Le 11/06/2012 13:07, Boris Hollas a ?crit : > Hello, > > both WP and Jessie (w/o apron) are unable to verify the following code: > > Jessie is unable to verify lemma rp, WP is unable to verify the > preconditions for the function calls in main. What is the problem here? -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120611/c40cfd1f/attachment.html>