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



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