--- 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?



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