--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2012 ---
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