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

[Frama-c-discuss] [Jessie Plugin] Can we trust prover CVC3 version 2.1 ?



Hi,

this is a bug in Why itself, and not a CVC3 bug. This will be fixed in 
the next Jessie/Why release.

In the meantime, do not use CVC3 2.1, please.

- Claude

Rousset Nicolas wrote:
>
> Hello,
>
> I found that CVC3 version 2.1 says produces a false positive on some 
> VCs related to integer overflow safety.
>
> The simple program below is an example where the second integer 
> overflow VC is valid for CVC3 2.1:
>
> -----------------------------------------------------
>
> typedef struct { int balance; } purse;
>
> //@ requires \valid(p);
>
> void credit(purse* p, int s) {
>
> p->balance += s;
>
> }
>
> -----------------------------------------------------
>
> Version 1.5 of CVC3 seems correct on this example (?timeout? for the 
> same VC).
>
> - Nicolas
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> 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


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |