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: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 4 Oct 2013 10:50:01 -0300
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: siteZero.c
Type: text/x-csrc
Size: 352 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131004/2d5d7705/attachment.c>