--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem in example of ACSL Implementation



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