--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



Hi,
         Are you using Frama-C Beryllium with CVC3? Or is it Boron version?

Kalyan

On Sat, May 15, 2010 at 2:01 AM, Naghmeh Ghafari <naghmeh.ghafari at cslabs.com
> wrote:

>
>  I was only asking whether alt-ergo and CVC3 were both proving the
>> post-condition, and whether they were both proving its negation.
>> If they are, we should look in a bug in Frama-C/Jessie/Why. If only
>> one of them is proving the property and its negation, we'll start
>> by suspecting a bug in that theorem prover. If you are using
>> Why's graphical interface, that would be the contents of the
>> row that corresponds to the post-condition.
>>
>
> Yes, they are both proving the post condition and its negation.
>
> cheers,
> naghmeh
>
>
>
> _______________________________________________
> 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
>



-- 
--
Kalyan KRISHNAMANI
http://www.tcs.tifr.res.in/~kalyan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100515/ae9a9274/attachment.htm>