--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Assert clause not proved



You can use ghost variables to prove correctness of the same code (see
attached). Alt+Ergo and Gappa prove correctness of this source.


---
Eugene Kornykhin,
Lomonosov Moscow State University


On 4 October 2013 17:50, Rovedy Aparecida Busquim e Silva
<rovedy at ig.com.br>wrote:

> Hi,
>
>
> The attached source code is a simplified version of the program we are
> trying to prove.
> Basically, M and L are struct type variables.
>
> L.M1 is equal to 0.0 and we tried to state this in the requires clause
> with the BOUND define. Is it correct?
>
> We want to prove that M.x1 and result variable are equal to 0.0 too,
> but the assert clauses are not proved. What is wrong?
>
> We are using the Jessie plug-in, Why3 Verification Platform 0.81,
> Fluorine-20130601 and the provers Alt-Ergo 0.95.2, CVC3 2.4.1, Gappa
> 1.0.0 and Z3 4.3.2.
>
> Best regards,
> Nanci, Luciana, Rovedy
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/4142f0ad/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: siteZero.c
Type: text/x-csrc
Size: 503 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/4142f0ad/attachment.c>