--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on July 2011 ---
Hello, Le mar. 26 juil. 2011 12:32:08 CEST, mars Gu <marsishandsome at gmail.com> a ?crit : > I have some questions about the Frama-c plug-in WP. > I know, that WP is now still under development. > I want to know, whether WP support or will support "Axiom" and "Separated > memory model"? > If yes, then how could I use these two features from the command line? I'm not too sure of what you mean by that. Could you be more specific about the issue involved? If your first point concern ACSL's axiom, then yes, WP supports them (apparently, there are still some subtleties regarding the presence of labels, though). If your second point is about \separated, again yes WP supports it. On the other hand, and unlike Jessie, it does not attempt to establish separation assumptions by itself, you have to provide them by hand. The only hypothesis that is done by default (option -wp-logicvar) is pointers do not point to variables whose address is not taken explicitly in the whole program. I hope that it helps, but again I may have misunderstood your question. Feel free to ask for more details. -- E tutto per oggi, a la prossima volta. Virgile