--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on November 2013 ---
Hello David, 2013/11/12 David Yang <abiao.yang at gmail.com>: > Thank you very much for answering my two such bad questions as I am a > beginner of formal verification and wp/jessie plugin. We are all beginners. And such tools can be quite complex at times. > 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. In fact, for any non trivial contract (and probably also for trivial ones), you'll need some annotations on loops. > If a function with many more loops, it will need a lot of work on > writing and checking those loop assign clauses. This is the price to pay for the strong guaranties provided by WP and Jessie plug-ins (after all, we are speaking of exhaustive testing). My rough estimate is that you need to double the size of your code with annotations (contract + loop) to be able to prove it. In an ideal world, programmer would not produce "important" code (safety critical or commercial code) without such annotations. We are very far from it to say the least but it is up to us to build such a world. > So Is there any automatic method or frama-c plugin(except the > GenAssigns plugin that Lo?c mentioned) that can do it for us ? Not that I am aware of. If your loops have small, known, bounds, you might have more luck with Value analysis plug-in. Value analysis needs less annotations, at the expense of verifying somewhat simpler properties (e.g. absence of Run Time Errors). Of course, your mileage may vary a lot depending on your actual code, properties you want to prove, way to express those properties in ACSL, etc. Best regards, david