--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on November 2013 ---
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>