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

  • Subject: [Frama-c-discuss] WP: Checking for invalid preconditions
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Wed, 19 Dec 2018 08:00:28 +0100
  • In-reply-to: <32712_1545117820_5C18A07C_32712_14173_1_af3eb5a3-5326-2854-0d37-46a862d37f90@cea.fr>
  • References: <79b956f3-a70e-194e-57b6-477d1563de66@physik.tu-berlin.de> <32712_1545117820_5C18A07C_32712_14173_1_af3eb5a3-5326-2854-0d37-46a862d37f90@cea.fr>
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.