Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>