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] Code proved with Fluorine is more proved with Neon

  • Subject: [Frama-c-discuss] Code proved with Fluorine is more proved with Neon
  • From: christophe.garion at isae.fr (Christophe Garion)
  • Date: Fri, 30 May 2014 01:19:16 +0200
  • In-reply-to: <5385B6B5.9060209@inria.fr> ("Claude \=\?utf-8\?Q\?March\=C3\=A9\=22\?\= \=\?utf-8\?Q\?'s\?\= message of "Wed, 28 May 2014 12:13:09 +0200")
  • References: <87mwe3sjnb.fsf@suntof.isae.fr> <5385B6B5.9060209@inria.fr>
Claude March? <Claude.Marche at inria.fr> writes:

> Le 27/05/2014 10:36, Christophe Garion a ?crit :
>> z3 4.3.1 via why3 seems to prove all the assertions under Neon, so it
>> may be an Alt-Ergo problem.
>
> External provers are not supposed to be equivalent, so this is non-sense
> to say that there is a problem with a prover X if it does not prove
> something that is proved by a prover Y.

Yes, you are right of course, sorry for my mistake. I just wanted to
precise that all the assertions can be proved, but not with Alt-Ergo as
previously.

Christophe

-- 
Christophe Garion          ISAE/DMIA - SUPAERO/IN
garion at isae.fr             10 avenue Edouard Belin
T?l : (33)5 61 33 80 57    BP 54032
Fax : (33)5 61 33 83 45    31055 Toulouse Cedex 4