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

In order to complete this work around, you can use in addition  the option
-wp-prop="complete_behaviors_unsatisfiable_requirements"
to focus only on detection of inconsistencies in preconditions
with eventually a lower time out (-wp-timeout=3 may be enough in practice) .

The opposite option
-wp-prop="-complete_behaviors_unsatisfiable_requirements"
allow you to disable this detection, and focus on the other properties.

-- Patrick Baudin

> 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' property 
> 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.