--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why wp plugin failed to prove such naive properties?



Hello David,

2013/11/10 David Yang <abiao.yang at gmail.com>:
> Why I can't prove the property B and C? I only get the minimal value of the
> array A.
>
> But it seems that the property B and C are obviously correct.
>
> Why it failed to prove these properties?

Because your are missing a "loop assigns" statement. "The absence of
'loop assigns i' is interpreted by 'loop assigns \everything' in the
WP." (Lo?c Correnson)

Loops are always an issue and should be treated with care in WP and Jessie.

This was discussed previously:
  http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-September/thread.html#3830
  http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-September/003831.html

Exercise: solve your issue without looking at attached file. ;-)

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q15_assigns.c
Type: text/x-csrc
Size: 623 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/e374f08e/attachment-0001.c>