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 ?

  • Subject: [Frama-c-discuss] [Jessie Plugin] Can we trust prover CVC3 version 2.1 ?
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
  • Date: Mon, 16 Nov 2009 11:18:58 +0100
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091116/ddea93b6/attachment-0001.htm