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

  • Subject: [Frama-c-discuss] WP: Checking for invalid preconditions
  • From: jaseg at physik.tu-berlin.de (Sebastian Götte)
  • Date: Tue, 18 Dec 2018 11:29:21 +0900
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