Both ANSI C and MSVC say that the pointer inequality p < q results in undefined behavior if p and q are not in the same object (or one past the last object of an array). VCC should assert that p an...
Id #6648 | Release:
None
| Updated: Mon at 5:07 PM by erniecohen | Created: Mon at 5:07 PM by erniecohen
Consider the problem of transferring ownership of an open object from one thread to another. Currently, there is no decent way to do this, because the usual method (transferring ownership through a...
Id #6647 | Release:
None
| Updated: Mar 24 at 5:28 PM by erniecohen | Created: Mar 24 at 5:28 PM by erniecohen
I have installed this release and I am getting the following error "Exception has been thrown by the target of an invocation" when I run VS 2010 or VS 2012. I have uninstalled VCC and the problem i...
Id #6646 | Release:
None
| Updated: Mar 19 at 3:01 PM by AntonDergunov | Created: Mar 19 at 3:01 PM by AntonDergunov
The following fails with the error:
"assertion 's is closed (for atomic(...)) did not verify."
It gets the same error if s is made _(read_only).
_(typedef struct S {} S)
void test(_(ghost...
Id #6645 | Release:
None
| Updated: Feb 25 at 12:50 AM by erniecohen | Created: Feb 25 at 12:49 AM by erniecohen
currently, \mine can take a list of objects, but not an \objset.
Id #6644 | Release:
None
| Updated: Feb 11 at 7:56 PM by erniecohen | Created: Feb 11 at 7:56 PM by erniecohen
the following function definition gets the error
"trigger must mention all quantified variables, but does not mention: Q#__vcc_state$1^3.42#tc1#344"
_(def \bool closed(\object o) {
return o->\cl...
Id #6643 | Release:
None
| Updated: Feb 5 at 9:43 AM by erniecohen | Created: Feb 5 at 9:43 AM by erniecohen
consider a function with a contract that takes an object argument which it writes, and returns either that object or another, fresh object. In either case, the returned object will be writable for ...
Id #6642 | Release:
None
| Updated: Feb 4 at 5:41 PM by erniecohen | Created: Feb 4 at 5:41 PM by erniecohen
VCC currently requires that pure functions terminate. This is inconvenient for predicates used to define recursive data structures. For example, we would like to define the nodes of a list with a d...
Id #6641 | Release:
None
| Updated: Jan 7 at 8:29 PM by erniecohen | Created: Jan 7 at 8:29 PM by erniecohen
The following fails to verify without the loop invariant that q >= 0:
_(void div(\natural n, \natural d _(out \natural q) _(out \natural r))
_(requires d > 0)
_(ensures n == q * d + r && r...
Id #6640 | Release:
None
| Updated: Jan 7 at 5:17 PM by erniecohen | Created: Jan 7 at 5:17 PM by erniecohen
Officially, a _(def) function should be a pure ghost function with an implicit postcondition derived from its body. This means that it should accommodate additional postconditions. However, while s...
Id #6639 | Release:
None
| Updated: Jan 5 at 8:37 PM by erniecohen | Created: Jan 5 at 8:37 PM by erniecohen