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?

Hi,

This is now fixed in Alt-Ergo's master branch:

https://github.com/OCamlPro/alt-ergo/issues/11

- Mohamed.

-- 
Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.info


Le 27/01/2016 15:24, Wolfram Kahl a écrit :
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160128/c154730b/attachment.html>