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] What is the point of ``All models'' in Alt-Ergo?

On Wed, Jan 27, 2016 at 09:40:33AM +0100, Claude Marché wrote:
> 
> By default, to prove a goal from a set of hypotheses, Alt-Ergo negates
> the goal and attempts to establish unsatisfiability.
> 
> With the experimental and undocument options related to "models", the
> goal is not negated anymore, hence the wrong results you get.

Thank you! So it is not due to the experimental nature, but due to the design...

Given the fact that Frama-C exposes access to Alt-Ergo's options
essentially via a simple double click on the goal,
it might be useful to document from the Frama-C side
which options of Alt-Ergo could be useful for Frama-C users,
and which are unsafe/forbidden.
(Since currently, Frama-C still picks up a green bullet for that falsum...)


Wolfram