--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on November 2013 ---
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