Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why wp plugin failed to prove such naive properties?

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