All integers are equal to 17

Jan 8, 2011 at 6:27 PM

VCC verifies the following code:

#include <vcc.h>

void foo(int *p)
maintains(wrapped(p))
ensures(*p == 17)
{
	;
}


void bar(int *p)
maintains(wrapped(p))
writes(p)
ensures(*p == 17)
{
	*p = 0;
}


typedef struct
{
	int a;
	invariant(a > 0)
} S;


int foobar(S *s) 
maintains(wrapped(s))
writes(&s->a)
ensures(result == 17)
{
	s->a = -1;
	return s->a;
}
I use the version from Dec 21st. What is wrong here?

Coordinator
Jan 8, 2011 at 7:01 PM

Hi,

  the problem here is the requirement on "int *p" being wrapped. In VCC, only objects can be wrapped, and, since "p" is a pointer to a primitive, not an object, this requirement introduces an inconsistency. This is also exhibited by the following minimal example:

#include <vcc.h>

void foo(int *p)
  requires(wrapped(p))
{
  assert(0);
}

  From the inconsistency, anything can be shown.

  (With the /smoke option, VCC will point out "unreachable code" in all the functions foo(), bar(), and foobar() of the original example, which may indicate problems like these).

  Hope this helps, Mark

 

Jan 10, 2011 at 5:07 PM

Hello,

since C has no objects, I assume you mean variables of a struct type. However, in the last example, s is a pointer to a struct, and both invariant and postcondition are violated.

For primitive types, do you have to use thread_local instead? Can type invariants be defined and verified for primitive types?

Regards,

Boris

Coordinator
Jan 10, 2011 at 6:35 PM

Hi,

  sorry, yes, I meant object pointers in the VCC sense, which include pointers to structs.

  The problem in the foobar() is indeed a little bit different: if an object is in a wrapped state, its fields may not be written to, which contradicts the write clause. Again, from the contradictory requirements, anything can be derived. Note that invariant is not checked in the implementation of foobar(); invariants are checked when objects are wrapped, and because no writes are allowed (and invariant admissibility) the invariant continues to hold while the objects remains closed. (See Section 5 of the tutorial, http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-1col.pdf for more details on that. Also, the related discussion http://vcc.codeplex.com/Thread/View.aspx?ThreadId=234338 may provide some additional examples).

  For primitive types you can use "requires(thread_local(x))" for reading. For writing "requires(mutable(x)) writes(x)" can be used, or even just "writes(x)", which implies the precondition on mutability.

  Unfortunately, no type invariants can be defined and verified for primitive types. There's a suggestion to do something like that (http://vcc.codeplex.com/workitem/3389).

  Best, Mark

 

Jan 11, 2011 at 11:42 AM

Hi Mark,

thanks for the link to that other thread, which explains writes and wrapped.

Boris