--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on June 2009 ---
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 |