--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on December 2018 ---
Hi, Unfortunately, there is nothing yet into WP for checking unsatisfiability of function requirements. But, there is below a better work around to achive what you done: - Just add this into your function contract:    behavior unsatisfiable_requirements:         assume \false;     complete behaviors unsatisfiable_requirements; - Then, a successful proof of a such 'complete behaviors' properties means your function requirements are unsatisfiable. The benefit of this method is it won't call in question the proof results of the other properties. -- Patrick Le 18/12/2018 à 03:29, Sebastian Götte a écrit : > 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