---
layout: fc_discuss_archives
title: Message 82 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?
- 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