--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on May 2010 ---
I believe it is Frama-C Beryllium that comes with ubuntu 10.04. naghmeh On 15/05/10 1:10 AM, Kalyan wrote: > 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 <mailto: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 > <mailto: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 <http://www.tcs.tifr.res.in/%7Ekalyan> > > > _______________________________________________ > 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 -- Naghmeh Ghafari, Ph.D. Research Associate Critical Systems Labs, Inc. Tel: (604) 638 7393 Cell: (778) 994 4802 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100517/6eb83a40/attachment.htm>