--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Approach to compute if-else in Wp and Why



The passification transformation in WP is done on-the-fly BY the memory model.
Actually, WP put the logical variables modeling the heap into passive form, not the C-code itself.
The situation is the same with Jessie : the passification is done on a why-2 program which is a translation of the C-code w.r.t Jessie's memory model.
	L.


Le 11 oct. 2012 ? 17:42, Boris Hollas a ?crit :

> On 11.10.2012 17:03, Lo?c Correnson wrote:
>> Recent developments in WP uses a variant of Leino's passication, but only for the experimental model "Typed" (in Oxygen).
> 
> And what do you use by default?
> 
> If both WP and Why use (or plan to) passification, maybe it would be useful to integrate the passification transform in Frama-C?
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss