--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on July 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Does WP support "Axiom" and "Separated memory model"?



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