--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floating point computations with WP and Jessie



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>