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: abiao.yang at gmail.com (David Yang)
  • Date: Tue, 12 Nov 2013 11:06:49 +0000
  • In-reply-to: <CAC3Lx=aj7HEYwjLe3OiAHouSfc+a0-Jy+R3wH+HroFfRD8D4DA@mail.gmail.com>
  • References: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com> <CAA1cxuiEdCsi613dVYe08-dhcpGNKCd684ZiAnpWHmU3WspM+w@mail.gmail.com> <CAC3Lx=aj7HEYwjLe3OiAHouSfc+a0-Jy+R3wH+HroFfRD8D4DA@mail.gmail.com>
Dear David:

On 12 November 2013 08:10, David MENTRE <dmentre at linux-france.org> wrote:
>
> from L1, L2, ... are NOT assigned. But it does NOT say that L1, L2,

Oops, While i reading this manual, i ignored this section by
considering the assigns clause is the same with the ensures clause.

Thank you very much for reminding me of this part.

david