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] Why wp plugin failed to prove such naive properties?

  • Subject: [Frama-c-discuss] Why wp plugin failed to prove such naive properties?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 12 Nov 2013 09:28:15 +0100
  • In-reply-to: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com>
  • References: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com>
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>