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

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.)

For example in

class A {

/*@ requires i > 0;
 requires i < 0;
 ensures \result == i+1;
*/
int m(int i) {
  return i;
}
};


the requires clauses are jointly unsatisfiable, so the erroneous ensures clause does not fail. If you add an 
'ensures \false;', the proof still does not fail, alerting you that something is wrong...

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.

- David
________________________________________
From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of Sebastian Götte [jaseg at physik.tu-berlin.de]
Sent: Tuesday, December 18, 2018 3:29 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: [Frama-c-discuss] WP: Checking for invalid preconditions

Hi,

is there some way to make WP check function requirements for satisfiability and barf if they are provably unsatisfiable? I just ran into this problem that one of my function specs accidentially included a unsatisfiable \separated predicate, leading frama-c to happily prove 1 == 2 (or anything else).

> struct foo {
>     char foo[32];
> };
>
> /*@ requires \separated(foo, &foo->foo);
>     ensures 1 == 2;
>   @*/
> int foo(struct foo * const foo) {
>     return -1;
> }

And the verification:
> dev~/r/l/src <3 frama-c -wp -wp-rte -wp-model +cint test.c
> [kernel] Parsing test.c (with preprocessing)
> [rte] annotating function foo
> [wp] 1 goal scheduled
> [wp] Proved goals:    1 / 1
>   Qed:             1

I mean, it would have caught the unsatisfiable \separated precondition at the callsite, but I think it would have been useful had it already caught this while proving function annotations. As-is, if ran on a source file containing only the function definition without the function being called anywhere, it will output something like "Proved goals 99/99" even if there is some trivial contradiction in one of the specifications.

Best regards,
Sebastian
_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss