--- layout: fc_discuss_archives title: Message 12 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,

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