--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2016 ---
[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