--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Predicate call not listed in jessie gui



I need to apologize, I just discovered the PO of question.

Thank you very much for your hint

Christoph
----- Original Message ----- 
From: "Virgile Prevosto" <virgile.prevosto at cea.fr>
To: <frama-c-discuss at lists.gforge.inria.fr>
Sent: Monday, April 20, 2009 10:26 AM
Subject: Re: [Frama-c-discuss] Predicate call not listed in jessie gui


> Hi Christoph,
>
> Le lun 20 avr 2009 10:11:20 CEST,
> "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :
>
>> When proving with jessie gui, I do not get any error but the 
>> predicate-call is neither listed nor does it seem to be proven.
>>
>
> I'm unsure of what you mean exactly: with Frama-C Lithium and why 2.17,
> there is a proof obligation related to the post-condition
> swapped{...}(...), and it is proved by alt-ergo, Z3 and Simplify. In
> fact, there are 5 PO, one for each ensures clause and assigns clause of
> the specification (+ 3 more for safety, but this is not related to your
> function contract). What is the PO that you expected to find in Why's
> output and which is not there?
>
> Best regards,
> -- 
> Virgile Prevosto
> Ing?nieur-Chercheur, CEA, LIST
> Laboratoire de S?ret? des Logiciels
> +33/0 1 69 08 71 83
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss