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] [Jessie] Assert clause not proved

  • Subject: [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: kornevgen at gmail.com (Eugene Kornykhin)
  • Date: Tue, 8 Oct 2013 11:11:03 +0400
  • In-reply-to: <CAEtoXR0kvDu5+NMAqEmCQkpQJRuGcagAZnURjAth_m=wxyQK+g@mail.gmail.com>
  • References: <CAEtoXR0kvDu5+NMAqEmCQkpQJRuGcagAZnURjAth_m=wxyQK+g@mail.gmail.com>
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>