--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2018 ---
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