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 S...
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
Verifying the following exhausts memory:
void assign(int v, int* pv)
_(writes pv)
_(ensures *pv == v);
void test();
void foo()
{
int local_a;
assign(3, &local_a);
test();
test...
Id #6638 | Release:
None
| Updated: Dec 20, 2012 at 6:16 PM by erniecohen | Created: Dec 18, 2012 at 6:06 PM by erniecohen
The following bombs VCC:
void test() {
_(ghost \natural x)
_(assert x && x)
}
Id #6637 | Release:
None
| Updated: Dec 11, 2012 at 7:26 PM by erniecohen | Created: Dec 11, 2012 at 7:26 PM by erniecohen
One of the challenges of a first-order approach to data structures is guaranteeing termination. For example, one way to formulate data structures is to maintain the reachability relation and insist...
Id #6636 | Release:
None
| Updated: Dec 10, 2012 at 10:44 AM by erniecohen | Created: Dec 10, 2012 at 10:44 AM by erniecohen
We have always maintained the invariant that only threads could own open objects. This has the advantage that we avoid silly errors arising from someone forgetting to put in an object invariant tha...
Id #6635 | Release:
None
| Updated: Dec 5, 2012 at 1:34 PM by erniecohen | Created: Dec 5, 2012 at 1:34 PM by erniecohen
Currently, _(always c,p) does not include a writes clause for c. However, a function will often take a derivative claim on c or change its ownership temporarily, either of which require writing c, ...
Id #6634 | Release:
None
| Updated: Nov 21, 2012 at 1:14 PM by erniecohen | Created: Nov 21, 2012 at 1:14 PM by erniecohen
The following fails to verify, because the second invariant forbids unwrapping (in the case that the succ of a List points to itself):
typedef struct List List, *PList;
typedef struct List {
vo...
Id #6633 | Release:
None
| Updated: Nov 15, 2012 at 3:49 PM by erniecohen | Created: Nov 15, 2012 at 3:49 PM by erniecohen
One of the most annoying aspects of ownership is that if an object is \wrapped but not \writable, it's ownership cannot be changed. This is crippling, because (1) it cannot be put into a container ...
Id #6632 | Release:
None
| Updated: Oct 18, 2012 at 10:20 PM by erniecohen | Created: Oct 18, 2012 at 10:20 PM by erniecohen
In the following, VCC can't prove termination of foo(). It succeeds if the type of the first argument to the constructor d2() is changed to int.
_(typedef _(record) struct S {
} S;)
_(datatype...
Id #6631 | Release:
None
| Updated: Oct 11, 2012 at 10:50 PM by MichalMoskal | Created: Oct 9, 2012 at 2:35 PM by erniecohen
Currently, listing an object in a writes clause implicitly requires it to be wrapped or mutable, and listing a field requires its embedding to be mutable. This has two big disadvantages. First, it'...
Id #6630 | Release:
None
| Updated: Sep 15, 2012 at 8:34 PM by erniecohen | Created: Sep 15, 2012 at 8:34 PM by erniecohen
The following gets a warning about possible assignment to physical memory from ghost memory:
void test1() {
_(ghost int x,y)
_(ghost x = y = 0)
}
Id #6629 | Release:
None
| Updated: Sep 13, 2012 at 11:06 AM by erniecohen | Created: Sep 13, 2012 at 11:06 AM by erniecohen
VCC requires that approvers be of type \object. It should allow any pointer type.
Id #6628 | Release:
None
| Updated: Sep 13, 2012 at 7:45 PM by MarkHillebrand | Created: Sep 13, 2012 at 10:59 AM by erniecohen
We have generally held that VCC is not obliged to catch syntactic errors that a C compiler is required to catch. This has generally been considered more of an excuse than a feature. I'm wondering w...
Id #6627 | Release:
None
| Updated: Sep 15, 2012 at 11:36 AM by erniecohen | Created: Sep 13, 2012 at 10:53 AM by erniecohen
The following causes confused death:
typedef struct S {
int x[10];
} S;
void test() {
S s,s1;
s = s1;
}
Id #6626 | Release:
None
| Updated: Sep 6, 2012 at 7:42 PM by erniecohen | Created: Sep 6, 2012 at 7:42 PM by erniecohen
See repro.
Id #6625 | Release:
None
| Updated: Aug 31, 2012 at 3:16 PM by MarkHillebrand | Created: Aug 31, 2012 at 3:14 PM by MarkHillebrand
We need to stratify the induction of abstract datatypes, to prevent a type from appearing as the domain of a map in one of its instances. Othwerwise, you get Russel's paradox. For example, the fo...
Id #6624 | Release:
None
| Updated: Aug 26, 2012 at 7:40 PM by erniecohen | Created: Aug 26, 2012 at 7:38 PM by erniecohen
Checked and unchecked are bad names to use for arithmetic. The difference has nothing to do with whether the arithmetic is checked; the difference is whether the arithmetic wraps (sadly, wrapped an...
Id #6623 | Release:
None
| Updated: Aug 24, 2012 at 8:08 PM by fdupress | Created: Aug 23, 2012 at 9:27 PM by erniecohen
Currently, any lemma marked {:bv} is implicitly _(unchecked). This is bad for a few reasons.
{:bv} is supposed to be something like a hint about how to prove the assertion. It should not be chang...
Id #6622 | Release:
None
| Updated: Aug 23, 2012 at 9:25 PM by erniecohen | Created: Aug 23, 2012 at 9:25 PM by erniecohen
Just as admissibility check functions are indicated by the tag _(admissibility), we should have a dedicated tag for reads checks (instead of using vcc_attr()). This is somewhat complicated by the f...
Id #6621 | Release:
None
| Updated: Aug 20, 2012 at 1:00 AM by erniecohen | Created: Aug 20, 2012 at 12:59 AM by erniecohen
We still pollute the namespace with vcc_attr. Even worse, it is hard to identify as being an annotation as opposed to being ordinary code. We should replace it with a tag (e..g _(attr).
Id #6620 | Release:
None
| Updated: Aug 19, 2012 at 11:25 PM by erniecohen | Created: Aug 19, 2012 at 11:25 PM by erniecohen
the following gets an error for undeclared identifiers, followed by a .bpl dump:
void test(int *a) {
a[a[0]] ++;
}
Id #6619 | Release:
None
| Updated: Aug 18, 2012 at 6:27 PM by erniecohen | Created: Aug 18, 2012 at 6:27 PM by erniecohen
(no further description required)
Id #6617 | Release:
None
| Updated: Aug 21, 2012 at 12:56 PM by stobies | Created: Aug 15, 2012 at 1:55 PM by erniecohen
The following assertions both fail.
void test() {
int *p;
_(assert \mutable_array(p,10) ==> p+10 > p)
_(assert \thread_local_array(p,10) ==> p+10 > p)
}
Id #6616 | Release:
None
| Updated: Aug 12, 2012 at 7:45 PM by erniecohen | Created: Aug 12, 2012 at 7:45 PM by erniecohen
We should add a universe type \U. There are several reasons to do so:
It would allow us to make polymorphic types using lock-style polymorphism. For example, if we want to make a polymorphic sequ...
Id #6615 | Release:
None
| Updated: Sep 15, 2012 at 11:37 AM by erniecohen | Created: Aug 11, 2012 at 9:30 AM by erniecohen
In a certain case inlining a member array into a struct fails with the following message:
(0,0) : error : use of undeclared function: $inlined_array
attempting to dump BPL to buggy.bpl
Verifica...
Id #6614 | Release:
None
| Updated: Aug 7, 2012 at 4:43 PM by yegord | Created: Aug 7, 2012 at 4:43 PM by yegord
currently, we have two very different ways to do a sequential read:
the target can be thread_local
the target can be a nonvolatile field of an object that is claimed to be closed (using _(by_clai...
Id #6613 | Release:
None
| Updated: Aug 5, 2012 at 3:47 PM by erniecohen | Created: Aug 5, 2012 at 3:27 PM by erniecohen
installing vcc on VS2012, the resulting installation is unable to verify files even from projects (the "reference not set to instance of an object" thing.)
Id #6612 | Release:
None
| Updated: Aug 21, 2012 at 7:42 AM by stobies | Created: Aug 1, 2012 at 5:19 PM by erniecohen
The following goes through, and therefore causes a trivially false axiom to be sent to Z3.
Having two declarations seem to be necessary to trigger the bug.
include <vcc.h>
_(abstract \natural toto...
Id #6611 | Release:
None
| Updated: Aug 1, 2012 at 10:52 AM by fdupress | Created: Aug 1, 2012 at 10:46 AM by fdupress
The following fails to verify:
typedef struct S {
int x;
} S;
void test() {
S x;
_(assert !\ghost(&x))
}
Id #6610 | Release:
None
| Updated: Jul 26, 2012 at 5:55 PM by erniecohen | Created: Jul 26, 2012 at 5:55 PM by erniecohen
VCC (as of version 2.3.724 at least) is not handling the sizeof() operator correctly.
The two code snippets below illustrate the issue.
See more samples and details in the related discussion a...
Id #6609 | Release:
None
| Updated: Jul 25, 2012 at 6:51 PM by MichalMoskal | Created: Jul 25, 2012 at 1:48 PM by edrdo
The explicit trigger in the example below shouldn't be needed.
typedef _(dynamic_owns) struct Queue {
_(ghost \natural len)
_(ghost PNode val[\natural])
_(invariant \forall \natural i; {val[i]} i...
Id #6608 | Release:
None
| Updated: Jul 24, 2012 at 3:49 PM by erniecohen | Created: Jul 24, 2012 at 3:49 PM by erniecohen
With aggressive pruning, admissibility check for a group may drop critical definitions of the enclosing structure, resulting in Buggy Boogie. (This is related to the syntax change in 7ed71cef38b6)....
Id #6607 | Release:
None
| Updated: Jul 20, 2012 at 9:53 AM by MarkHillebrand | Created: Jul 20, 2012 at 9:53 AM by MarkHillebrand
In some cases we want to express locally that the objects of a given type have unique identifiers.
The attached file contains code that illustrates how this works for structures and a failing/not ...
Id #6606 | Release:
None
| Updated: Jul 20, 2012 at 2:06 AM by MichalMoskal | Created: Jul 18, 2012 at 9:00 AM by hristopentchev
The following gets "OOPS: unhandled stmt stmt @begin_update":
void test() {
if (1) {
_(begin_update)
}
}
Id #6605 | Release:
None
| Updated: Jul 13, 2012 at 12:48 AM by erniecohen | Created: Jul 13, 2012 at 12:48 AM by erniecohen
A problem that frequently arises in writing functions is the need to constrain a local variable with an invariant. In particular, we often want to use a local variable to track some knowledge about...
Id #6604 | Release:
None
| Updated: Jul 4, 2012 at 3:33 PM by erniecohen | Created: Jul 4, 2012 at 3:33 PM by erniecohen
Today, volatile structs and unions are essentially useless, because there are no invariants constraining their fields. Nevertheless, they arise in real code.
I see two ways to fix this. My prefer...
Id #6603 | Release:
None
| Updated: Jul 4, 2012 at 3:04 PM by erniecohen | Created: Jul 4, 2012 at 3:04 PM by erniecohen
The following code produces
error VC0008: No overload for method '__Globals__.foo' takes '1' arguments.
void foo(void _(ghost int a))
;
void test()
{
_(ghost int a = 10;)
foo(_(ghost a));
}
Id #6602 | Release:
None
| Updated: Jul 4, 2012 at 2:05 PM by MikhailKovalev | Created: Jul 4, 2012 at 2:05 PM by MikhailKovalev
The following verifies:
void test() {
int x;
_(unchecked) x++;
}
According to the C standard, signed arithmetic overflow produces undefined behavior. I didn't find anything in MSDN to co...
Id #6601 | Release:
None
| Updated: Jul 30, 2012 at 11:57 PM by MichalMoskal | Created: Jul 3, 2012 at 5:26 PM by erniecohen
The following verifies. Note that if & is applied to some part of s, the problem goes away because VCC would then have to pick which union member is active.
typedef struct S {
int x;
} S;
typ...
Id #6600 | Release:
None
| Updated: Jul 31, 2012 at 12:21 AM by MichalMoskal | Created: Jun 28, 2012 at 9:07 PM by erniecohen
The following verifies:
void test()
_(ensures 0)
{
_(ensures 0)
{
}
}
Id #6599 | Release:
None
| Updated: Jul 31, 2012 at 12:01 AM by MichalMoskal | Created: Jun 19, 2012 at 12:22 PM by erniecohen
Record types are typically used to represent mathematical types. As such, they typically require some qualification to me be meaningful. A typical example is a permutation type, giving forward and ...
Id #6598 | Release:
None
| Updated: Aug 28, 2012 at 3:13 PM by erniecohen | Created: Jun 19, 2012 at 11:35 AM by erniecohen
The following causes VCC to dump boogie:
typedef struct S {
int x;
} S;
_(def S foo() {
S s;
s.x = 3;
return s;
})
Id #6597 | Release:
None
| Updated: Jul 31, 2012 at 12:36 AM by MichalMoskal | Created: Jun 19, 2012 at 3:35 AM by erniecohen
Currently, we do not check termination for loops in a function that does not itself have a termination measure. Presumably, this is because on a function call we wouldn't have a measure to compare ...
Id #6596 | Release:
None
| Updated: Jul 31, 2012 at 12:48 AM by MichalMoskal | Created: Jun 14, 2012 at 8:14 PM by erniecohen
malloc and free should have in their contracts _(decreases 0)
Id #6594 | Release:
None
| Updated: Jul 31, 2012 at 12:07 AM by MichalMoskal | Created: Jun 14, 2012 at 4:20 PM by erniecohen
The following gets the error "expression with side effects used in pure context {"
void test(unsigned len)
_(decreases 0)
{
for (unsigned i=0; i < len -1; i++)
{}
}
The error goes away if th...
Id #6593 | Release:
None
| Updated: Jun 14, 2012 at 3:56 PM by erniecohen | Created: Jun 14, 2012 at 3:17 PM by erniecohen
When a state change is made, we implicitly check first the invariants of all updated objects (in parallel), then all unupdated non-\claim objects (in parallel), then all \claims (in parallel). Howe...
Id #6592 | Release:
None
| Updated: Jun 10, 2012 at 1:27 PM by erniecohen | Created: Jun 10, 2012 at 1:27 PM by erniecohen
The following type should not verify; it should give an error tht the :lemma is not a lemma:
typedef struct S {
int x;
_(invariant :lemma \on_unwrap(\this, \false))
} S;
Also, the :lemma appea...
Id #6591 | Release:
None
| Updated: Jun 6, 2012 at 1:58 AM by erniecohen | Created: Jun 6, 2012 at 1:58 AM by erniecohen
The lemma in the following gets the error that it forbids unwrapping. This check should not be made for :lemma invariants, since they don't have to be checked on unwrapping anyway.
typedef struct...
Id #6590 | Release:
None
| Updated: Jun 6, 2012 at 12:46 AM by erniecohen | Created: Jun 6, 2012 at 12:46 AM by erniecohen
The following program verifies, because VCC fails to check the admissibility of the invariant of the inner struct.
typedef struct S {
int x;
struct T {
int y;
struct S *s;
_(invariant...
Id #6589 | Release:
None
| Updated: Aug 28, 2012 at 4:00 PM by stobies | Created: Jun 6, 2012 at 12:08 AM by erniecohen
The following causes confused death:
include <vcc.h>
_(datatype List {
case Nil();
case Cons(int x, List tail);
})
_(ghost void test() {
List l;
switch (l) {
case Nil(): break;
default: break;
}...
Id #6588 | Release:
None
| Updated: Jun 2, 2012 at 2:23 PM by erniecohen | Created: Jun 2, 2012 at 2:23 PM by erniecohen
The following dumps boogie:
typedef struct S {
int y;
} S;
void test() {
_(ghost S *s)
_(assert s \is s)
}
Id #6587 | Release:
None
| Updated: Jun 1, 2012 at 6:18 PM by erniecohen | Created: Jun 1, 2012 at 6:18 PM by erniecohen
\program_entry_point() is supposed to mean that all globals are mutable. This should not be allowed in an object invariant, because \me is meaningless there. Note, however, that this is probably ha...
Id #6586 | Release:
None
| Updated: Jun 1, 2012 at 5:01 PM by erniecohen | Created: Jun 1, 2012 at 5:01 PM by erniecohen
The following function gets the error "assignment to physical location from ghost code"
void test() {
_(ghost int x,y;)
_(ghost y = x = 2)
}
Id #6585 | Release:
None
| Updated: Jun 1, 2012 at 4:40 PM by erniecohen | Created: Jun 1, 2012 at 4:40 PM by erniecohen
The following verifies:
void test(int *x)
_(requires \mutable(x) && *x == 0)
_(writes x)
{
*x = (*x)++;
}
VCC correctly reports an error if *x is replaced by a local variable.
Id #6584 | Release:
None
| Updated: May 29, 2012 at 6:30 PM by erniecohen | Created: May 29, 2012 at 6:30 PM by erniecohen
Sadly, \object does not correspond to what we call objects; it corresponds to what we call pointers. This is not only gross and confusing; because objects are not a fully-fledged type, we don't cat...
Id #6583 | Release:
None
| Updated: May 28, 2012 at 12:04 AM by erniecohen | Created: May 28, 2012 at 12:04 AM by erniecohen
The following verifies (without the warning that would be generated without the block contract):
void test()
_(decreases 0)
{
_(ensures \true)
{
while (1) {}
}
}
I think the proper s...
Id #6582 | Release:
None
| Updated: May 27, 2012 at 12:56 AM by erniecohen | Created: May 27, 2012 at 12:54 AM by erniecohen
The following gets "confused, will now die"
void test()
{
_(decreases 0)
{
}
}
Id #6581 | Release:
None
| Updated: May 27, 2012 at 12:48 AM by erniecohen | Created: May 27, 2012 at 12:48 AM by erniecohen
The following verifies:
_(pure) int foo()
_(ensures \false)
{
int x;
while (1) {}
return x;
}
void test()
{
_(assert 0)
}
We assume that all pure functions are witnessed by mathematica...
Id #6580 | Release:
None
| Updated: May 26, 2012 at 7:45 PM by erniecohen | Created: May 26, 2012 at 7:45 PM by erniecohen
The following verifies:
_(pure) int foo() {
int x;
return x;
}
void test()
{
int x,y;
x = foo();
y = foo();
_(assert x==y)
}
This is sound for pure ghost functions, because the nondetermi...
Id #6579 | Release:
None
| Updated: May 26, 2012 at 11:42 PM by erniecohen | Created: May 26, 2012 at 7:23 PM by erniecohen
Right now, the syntactic restrictions under which \domain_updated_at verifies (not to mention error messages talking about skinny_expose (which we no longer expose, skinnily or otherwise)) are maki...
Id #6578 | Release:
None
| Updated: May 26, 2012 at 1:47 AM by erniecohen | Created: May 26, 2012 at 1:47 AM by erniecohen
This would allow using domain roots x in _(by_claim x) o->f, or to talk about such fields without creating additional claims (that would need write permissions on x)./
Id #6577 | Release:
None
| Updated: May 25, 2012 at 7:53 AM by MarkHillebrand | Created: May 25, 2012 at 7:53 AM by MarkHillebrand
With the previous fix to \claims and \make_claim (to make them implicitly wrap local variables in \when_claimed()) and the proposed fix to \at (to do the same thing for local variables), and writes...
Id #6576 | Release:
None
| Updated: May 25, 2012 at 7:47 AM by MarkHillebrand | Created: May 24, 2012 at 7:12 PM by erniecohen
Currently, _(by_claim c, e) can be used only to read nonvolatile fields. We should be able to use it to also read volatile fields; indeed, we should be able to use it to read through an arbitrary p...
Id #6575 | Release:
None
| Updated: Aug 5, 2012 at 2:35 PM by erniecohen | Created: May 24, 2012 at 2:52 PM by erniecohen
For local variables ocurring in \at, we should do the same thing that we do for local variables in \claims and \make_claim, i.e. implicitly wrap them in \when_claimed(). Needless to say, we should ...
Id #6574 | Release:
None
| Updated: May 25, 2012 at 7:59 AM by MarkHillebrand | Created: May 24, 2012 at 2:21 PM by erniecohen
A purely local variable is a local variable whose address is never taken. VCC treats such variables specially with respect to writes clauses; such variables don't have to be explicitly mentioned in...
Id #6573 | Release:
None
| Updated: Aug 28, 2012 at 3:02 PM by erniecohen | Created: May 21, 2012 at 4:28 AM by erniecohen
The following gets a "confused, will now die".
void test()
{
_(ensures \true)
{
}
}
Id #6572 | Release:
None
| Updated: May 21, 2012 at 3:57 AM by erniecohen | Created: May 21, 2012 at 3:57 AM by erniecohen
Using &\me in an expression gets an oops. Of course you should not be able to take the address of \me anyway.
Id #6571 | Release:
None
| Updated: May 22, 2012 at 7:04 AM by stobies | Created: May 20, 2012 at 6:29 PM by erniecohen
Currently, we allow \me to occur inside an object invariant. I believe this can be turned into an unsoundness, by having a \thread field th in the object with invariant th == \me (since different ...
Id #6570 | Release:
None
| Updated: Jul 31, 2012 at 12:18 AM by MichalMoskal | Created: May 20, 2012 at 6:27 PM by erniecohen
Instead of writing \on_unwrap(\this,p), we should write \on_unwrap(p).
Id #6569 | Release:
None
| Updated: May 20, 2012 at 6:06 PM by erniecohen | Created: May 20, 2012 at 6:06 PM by erniecohen
We currently pollute several C namespaces in a distressingly irregular way. We should instead reserve a more clearcut portion of each namespace, e.g. all identifiers beginning with _VCC.
Current...
Id #6568 | Release:
None
| Updated: Jun 1, 2012 at 2:23 PM by erniecohen | Created: May 19, 2012 at 5:00 PM by erniecohen
A common idiom that arises is that a thread knows Inv is stable because he owns some unclaimable object o. Unfortunately, he can't form a claim of this property directly, because the claim would be...
Id #6567 | Release:
None
| Updated: May 18, 2012 at 7:27 PM by erniecohen | Created: May 18, 2012 at 7:27 PM by erniecohen
some ghost operations are typed to return \integers when they should return \naturals (e.g. \size()), or naturals when they should return size_t (e.g. \sizeof_object())
Id #6566 | Release:
None
| Updated: May 18, 2012 at 1:40 PM by fdupress | Created: May 18, 2012 at 1:44 AM by erniecohen
the following fails to verify:
typedef struct T {
int x;
} T;
void test(T *t)
{
_(assume \wrapped(t))
_(assert !\ghost(t))
}
Id #6565 | Release:
None
| Updated: Jul 31, 2012 at 12:19 AM by MichalMoskal | Created: May 18, 2012 at 1:06 AM by erniecohen
The following should get a compiler error, but instead causes a stack overflow exception:
_(ghost typedef struct Foo {
struct Foo g;
} Foo;)
_(ghost void test () {
Foo f;
})
Id #6563 | Release:
None
| Updated: May 15, 2012 at 7:20 PM by erniecohen | Created: May 15, 2012 at 7:20 PM by erniecohen
Currently, pure functions (like other functions) implicitly require a full-stop state. This means that when they are useless inside an atomic action after the first effectfull update, or in an admi...
Id #6562 | Release:
None
| Updated: May 15, 2012 at 7:03 PM by erniecohen | Created: May 15, 2012 at 7:03 PM by erniecohen
In block contracts, we allow _(requires \full_context()) to have the block take in all information about the preceding context of the function, while limiting flow of information out of the block. ...
Id #6561 | Release:
None
| Updated: May 10, 2012 at 7:01 PM by fdupress | Created: May 10, 2012 at 5:50 PM by erniecohen
One of the goals of the switch to the new syntax (3 years ago) was to avoid polluting the C namespace (beyond the single macro _()). Currently, we still pollute it by #defining vcc_attr(). We shoul...
Id #6560 | Release:
None
| Updated: May 10, 2012 at 6:19 PM by stobies | Created: May 9, 2012 at 11:38 AM by erniecohen
_(admissibility) functions need to terminate for soundness. We should add _(decreases 0) to the implicit contract of such functions. (They cannot be added manually because explicit contracts are n...
Id #6559 | Release:
None
| Updated: May 14, 2012 at 12:43 PM by erniecohen | Created: May 9, 2012 at 2:21 AM by erniecohen
In the following program, VCC gives a warning that pointers of different types are never equal, but does not give an error on the assertion.
typedef struct Int {
int x;
} Int;
typedef union A ...
Id #6557 | Release:
None
| Updated: May 10, 2012 at 6:24 PM by stobies | Created: May 4, 2012 at 6:22 PM by erniecohen
The VCC policy is that we should be able to soundly translate a function call so that arguments are evaluated from left to right. This is violated by the following call, which verifies:
f(_(atomi...
Id #6554 | Release:
None
| Updated: May 10, 2012 at 6:38 PM by stobies | Created: May 2, 2012 at 10:27 PM by erniecohen
Currently VCC does not allow loops within atomics, because it does not allow gotos within atomics (and loops are translated to gotos). However, loops in atomics are useful, in particular when an un...
Id #6553 | Release:
None
| Updated: May 10, 2012 at 6:54 PM by stobies | Created: May 1, 2012 at 12:00 PM by erniecohen
The following program causes VCC to report "(0,0) : error : undeclared identifier : $bogus" and dump boogie. We should probably report an error here.
void test0(Foo *f)
_(requires \writable(f))
...
Id #6552 | Release:
None
| Updated: May 10, 2012 at 6:56 PM by stobies | Created: May 1, 2012 at 11:25 AM by erniecohen
The following gets the error "OOPS: unhandle macro &":
void test0(Foo *f)
_(writes &(f->\owns))
{}
Id #6551 | Release:
None
| Updated: May 17, 2012 at 10:58 AM by erniecohen | Created: May 1, 2012 at 5:06 AM by erniecohen
We should make \mutable apply to sets (casting non-sets to singletons), and depricate \extent_mutable. We should do likewise with \fresh. We should perhaps also make \zero apply to pointers, not ju...
Id #6549 | Release:
None
| Updated: May 10, 2012 at 7:03 PM by stobies | Created: Apr 30, 2012 at 2:08 AM by erniecohen
Currently, we do not provide an end-to-end way for a users to verify and run a multithreaded application. To make this possible, we should support kicking off a new thread, preferably in a way that...
Id #6548 | Release:
None
| Updated: May 10, 2012 at 6:49 PM by stobies | Created: Apr 29, 2012 at 1:31 AM by erniecohen
If a pure function has a _(decreases) clause, there is no reason to give a warning for a cycle in pure function calls. (Indeed, we should only give a warning if there is a cycle of functions, none ...
Id #6546 | Release:
Latest build, v2.1.20706.0
| Updated: Jan 5 at 8:08 PM by erniecohen | Created: Apr 27, 2012 at 12:19 PM by erniecohen
http://vcc.codeplex.com/workitem/6462 introduced dot syntax for meta fields (\owns, \closed, ...). In this specific case it doesn't seem to work:
struct A { int a; };
struct B { struct A A[2]; }...
Id #6545 | Release:
None
| Updated: May 10, 2012 at 7:08 PM by stobies | Created: Apr 25, 2012 at 7:12 AM by MarkHillebrand
The following test fails to verify:
include <vcc.h>
void test(void)
{
int *x, *y;
if (x == y)
{
_(assert x == y)
}
}
Id #6544 | Release:
None
| Updated: May 10, 2012 at 7:08 PM by stobies | Created: Apr 24, 2012 at 6:40 PM by mflorian
A common idiom is to take a wrapped object, temporarily pass ownership to some data structure, and take ownership back before returning. Two common examples are (1) where ownership has to be tempor...
Id #6543 | Release:
None
| Updated: Jul 12, 2012 at 12:51 PM by erniecohen | Created: Apr 24, 2012 at 2:45 PM by erniecohen
See attached file (or vcc\Test\testsuite\vcc2ns\records-19). This used to work previously.
Id #6541 | Release:
None
| Updated: May 10, 2012 at 7:13 PM by stobies | Created: Apr 16, 2012 at 1:58 PM by MarkHillebrand
The following program gets the error "approves(...) needs this->field as the second parameter":
typedef struct Foo {
volatile int x;
_(invariant \approves(\this->\owner,x))
} Foo;
typedef stru...
Id #6540 | Release:
None
| Updated: May 10, 2012 at 7:13 PM by stobies | Created: Apr 10, 2012 at 7:01 PM by erniecohen
Fields of a ghost union are treated as they are implementation fields and warning is generated:
[possible unsoundness]: assignment to physical location from specification variable 'a'
See attac...
Id #6538 | Release:
None
| Updated: May 10, 2012 at 7:14 PM by stobies | Created: Apr 3, 2012 at 11:19 AM by MikhailKovalev