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] Problem in example of ACSL Implementation

  • Subject: [Frama-c-discuss] Problem in example of ACSL Implementation
  • From: tienhm at gmail.com (Tien Hoang Minh)
  • Date: Mon, 29 Jun 2009 12:15:22 -0400
Hi everybody,
I run the example 2.15 (page 32, ACSL Implementation) with
FramaC/Jessie/Alt-Ergo Lithium version, the result is there are 33 VCs
in total but only 18 of them are valid. When I run separately Alt-Ergo
with the *_why.why file, there are many warning "Inconsistent
assumption". Is there any problem with this example ? In the loop
invariant, there is an association with the behavior failure (line
15), but in my opinion, it only happens when we can find an element of
array t that equals v (the case success) so I think we should
associate this loop invariant with the behavior success, Is there
something wrong in my comment ?
Please help me to solve all these. Thank you in advance.
BR
Tien.

PS: I attach the example with this message.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ex215.c
Type: text/x-csrc
Size: 735 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090629/867c139c/attachment.c