---
layout: fc_discuss_archives
title: Message 2 from Frama-C-discuss on May 2016
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin
- Subject: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin
- From: loic.correnson at cea.fr (Loïc Correnson)
- Date: Wed, 4 May 2016 13:54:47 +0200
- In-reply-to: <87fuu82u9r.fsf@inria.fr>
- References: <87fuu82u9r.fsf@inria.fr>
> /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */
This lemma is definitely wrong in WP with Real model (not float there).
At least, it is not provable in the forthcoming release of Frama-C.
Is there a bug in some existing release?
L.