--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on June 2009 ---
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