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 calculus

Hi,

Thanks for your interest in Frama-C.

Mauro Baluda a ?crit :
> what I need is to obtain the precondition that guarantees that the
> execution of a given C statement brings the program in a state
> fullfilling a given C (if possible) predicate... ex:
> 
> WP(x = x+1, x < 1) =(x<0)
> 
> the algorithms works on single paths so there is no need to calculate
> wp for loops...

Do you mean that loops are somehow statically unrolled ? Could you give 
a full example showing what you want to do?

> I would instead need to be able to calculate wp for assume statements
> and sequences of statements

The answer vastly depend on the logic used to write (x<1) and (x<0).
This is what Claude called a "memory model".
The choice depends on the fragment of C you want to support and on the 
kind of property you are willing to get.
Anne may show some possible outputs on your very example with different 
memory models.

You mention "C predicate": do you mean any side-effect free C expression 
  without function calls interpreted according to the semantics of C?

> In my dreams this would be given by an API usable directly in C...

To fulfill your dream you need to add C binding to Frama-C. This is far 
from being easy.


Hope this helps,
-- 
| Benjamin Monate         | mailto:benjamin.monate at cea.fr     |
| Head of Software Safety Lab.  CEA-LIST/DRT/DTSI/SOL/LSL     |