--- layout: fc_discuss_archives title: Message 83 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,

Thank you very much for answering my two such bad questions as I am a
beginner of formal verification and wp/jessie plugin.
I am grateful for your help.

Indeed, I need to read more carefully of those manuals.

On 12 November 2013 08:28, David MENTRE <dmentre at linux-france.org> wrote:
> 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. ;-)

Thanks for so kindness.
These information are very useful.
Under your suggestion, I solved these problems without looking at the
attached file.

If I have write the loop assign clause, I can verify many more functions.

But this also means that while i have function contract without any no
loop assign clause, I can't succeed verifying those kinds of functions
at all.

If a function with many more loops, it will need a lot of work on
writing and checking those loop assign clauses.

So Is there any automatic method or frama-c plugin(except the
GenAssigns plugin that Lo?c mentioned) that can do it for us ?

" In this digest, Lo?c mentioned about the GenAssigns plugin...
>> Jessie makes this kind of analysis and the (non-distributed) plugin GenAssigns infer missing assigns clauses like those.
"

Best regards,

-david