--- layout: fc_discuss_archives title: Message 60 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



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>