Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |