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

inconsistencies with structs

The following verifies with the switch /z:MBQI=true: (struct P {} ;) void test() { _(assert \false) } The following also verifies (with the same switches): typedef struct S { int x; } S; void tes...

Id #6654 | Release: None | Updated: Aug 31, 2015 at 4:43 PM by erniecohen | Created: Aug 27, 2015 at 1:19 AM by erniecohen

pure functions introduce inconsistency

The following verifies with the switch /b:MBQI=true: _(pure) int f(); _(void test() { _(assert f() == f()) _(assert \false) }) The following verifies with default switches: _(pure) int f() _(ensur...

Id #6653 | Release: None | Updated: Aug 26, 2015 at 8:44 PM by erniecohen | Created: Aug 26, 2015 at 3:51 PM by erniecohen

Visual Studio IDE doesn't work for VCC

I installed the VCC according to the instruction for several times. But the visual studio IDE doesn't work for VCC. When I right click some function there is no verification option. But the command...

Id #6652 | Release: None | Updated: Oct 27, 2014 at 6:54 PM by wenrui | Created: Oct 27, 2014 at 6:54 PM by wenrui