--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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