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] WP: Checking for invalid preconditions

To answer Yannick, In OpenJML
1) You can add a check manually by inserting '//@ reachable;' in the body of a method.
2) With command-line options you can check lots of different places: after preconditions (before function body), just before explicit asserts, just after explicit assumes, at the exit of the method, at the beginning of branches, at each return/throw point etc.
3) OpenJML also handles feasibility tests specially, only reporting a problem if an intentional feasibility check shows that the given program point is unreachable.

- David
________________________________
From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of Yannick Moy [moy at adacore.com]
Sent: Tuesday, December 18, 2018 9:51 AM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] WP: Checking for invalid preconditions

-- COK David (2018-12-18)
The way to do this manually is to put something unprovable at the end of the function - e.g. at the return or as a last postcondition. If WP does not complain about it then something in all the assumptions to that point is unsatisfiable.
(This is common enough that OpenJML for Java programs automatically attempts a feasibility check whevener a proof succeeds.)

In OpenJML, do you simply add such a check at the end of each function? That's one point to check, but possibly not the only one, and it does not allow detecting inconsistencies in preconditions if the body of the function is not analyzed.

In SPARK, we have added recently such checking in various places, at the request of customers:
- to detect inconsistent preconditions (independently of the analysis of the function itself)
- to detect postconditions always false
- to detect dead code after loops (because of the risk of not proving loop termination leading to unsoundness)
- to detect unreachable branches in assertions and contracts (because complex contracts may lead to confusion that can be detected this way)

Unfortunately, on realistic problems, it can take quite a bit longer (in my experience) to determine satisfiability than unsatisfiability, particularly if there are many quantified axioms. Consequently adding infeasibility checks can add time to proof checking.

We also had the same experience, so we limited this checking to: only one prover called for each of these, with a timeout of 1 second. And we also did not enable it by default, people have to use a switch (--proof-warnings). And we handle these specially, so that we get only warning messages when there is an issue, and nothing when the unreachability property is not proved.

But we also recommend enabling it, as it found surprising problems in our own testsuite. :-)
In particular, the test for unreachable branches in assertions/contracts is something that I recommend implementing in other tools.

--
Yannick Moy, Senior Software Engineer, AdaCore



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181218/27d78864/attachment.html>