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 5:48 PM by erniecohen | Created: Mar 14 at 5: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 7:38 PM by erniecohen | Created: Mar 13 at 7: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 7:29 PM by erniecohen | Created: Feb 27 at 2: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 8:53 PM by erniecohen | Created: Aug 27, 2016 at 8: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 1:56 PM by erniecohen | Created: Jul 19, 2016 at 1: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 1:49 PM by erniecohen | Created: Jul 19, 2016 at 1: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 11:15 PM by erniecohen | Created: Jul 14, 2016 at 11: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 4:13 PM by erniecohen | Created: Feb 11, 2016 at 4:13 PM by erniecohen

Problem with nested structs?

Does VCC have difficulties handling nested structs? In the code below VCC complains when assigning a struct to a member of a struct that is a struct itself: include <vcc.h> typedef struct date { ...

Id #6656 | Release: None | Updated: Feb 11, 2016 at 4:23 PM by erniecohen | Created: Dec 10, 2015 at 9:26 AM by dgurov

owner-approved fields cannot be encapsulated

The VCC framing discipline allows updates to the fields of an object o to he hidden in the contract of an operation that operates on a wrapped o, because opening up o gives the thread the right to ...

Id #6655 | Release: None | Updated: Oct 6, 2015 at 12:48 AM by erniecohen | Created: Oct 6, 2015 at 12:43 AM by erniecohen