Not able to verify

unsigned mult (unsigned n, unsigned m) _(requires m >= 0 && m <= UINT_MAX && n*m <= UINT_MAX) _(ensures \result == n*m) { unsigned a = 0; unsigned x = 0; while (x < m) _(invariant ...

Id #6666 | Release: None | Updated: Mar 29 at 3:54 AM by inzemam | Created: Mar 29 at 3:54 AM by inzemam

Unsoundness?

Hi, Consider the following code: int x; void foo() _(ensures x == \old(x)) { } This code verifies... but should not? Shouldn't x be able to obtain any value during the execution of foo? ...

Id #6665 | Release: None | Updated: Mar 23 at 9:40 AM by fat_jonass | Created: Mar 23 at 9:40 AM by fat_jonass

def function transparency principle

We generally want to encourage the use of def functions, rather than macros. Def functions provide better diagnostic for failed verifications, provide useful hooks for triggering, for providing add...

Id #6664 | Release: None | Updated: Mar 14 at 4:48 PM by erniecohen | Created: Mar 14 at 4:48 PM by erniecohen

violation of declaration-quantification duality

Consider the following two fragments: { T x; _(assert p) } vs _(assert \forall T x; p) Assuming that T is a type not requiring initialization (e.g. \integer) I believe it should be a pri...

Id #6663 | Release: None | Updated: Mar 13 at 6:38 PM by erniecohen | Created: Mar 13 at 6:38 PM by erniecohen

Unsoundness when verifying code with variables declared as static

Hello, The following code is verified in VCC although the assertion clearly does not hold. include <vcc.h> void main() { stat(); stat(); } void stat() { static int s=0; _(asse...

Id #6662 | Release: None | Updated: Mar 13 at 6:29 PM by erniecohen | Created: Feb 27 at 1:12 PM by fat_jonass

VCC should check memory initialization for reads of concrete locations

VCC doesn't check that memory that is read has been initialized. While this feature is useful for ghost memory (it provides a convenient encoding of nondeterministic choice), standard C mandates th...

Id #6661 | Release: None | Updated: Aug 27, 2016 at 7:53 PM by erniecohen | Created: Aug 27, 2016 at 7:53 PM by erniecohen

records should allow pointwise updates to map members

We should allow updates like the following, where f is a field of o of map type: o = o / {.f[0] = 0} ;

Id #6660 | Release: None | Updated: Jul 19, 2016 at 12:56 PM by erniecohen | Created: Jul 19, 2016 at 12:56 PM by erniecohen

unsoundness in unions with multiple members with same object type

the following verifies: typedef struct S { int x; } S; typedef union U {S s1; S s2; } U; void test() { U u; _(union_reinterpret &u.s2) _(assert 0) }

Id #6659 | Release: None | Updated: Jul 19, 2016 at 12:49 PM by erniecohen | Created: Jul 19, 2016 at 12:49 PM by erniecohen

missing check on claim destruction in atomics

The soundness of treating atomic actions as atomic depends on the objects in the closed object list remaining closed for the duration of the atomic. By historical accident, VCC implements this with...

Id #6658 | Release: None | Updated: Jul 14, 2016 at 10:15 PM by erniecohen | Created: Jul 14, 2016 at 10:15 PM by erniecohen

flexible array members unsound

VCC doesn't promise support for flexible array members, but currently silently treats them unsoundly. In particular, the footprint of a flexible array member does not correctly alias the memory fol...

Id #6657 | Release: None | Updated: Feb 11, 2016 at 3:13 PM by erniecohen | Created: Feb 11, 2016 at 3:13 PM by erniecohen