Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Does WP support "Axiom" and "Separated memory model"?
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Fri, 29 Jul 2011 10:33:23 +0200
  • In-reply-to: <CAE6MND6s9=n9-oYR_JPNa5vMVqUEUa+X+vp-KKf-Gv-uYN6+qg@mail.gmail.com>
  • References: <CAE6MND6s9=n9-oYR_JPNa5vMVqUEUa+X+vp-KKf-Gv-uYN6+qg@mail.gmail.com>
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