Hi,

There seems to be something wrong with the way VCC handles the sizeof operator (or at least in the version I'm using; see version info below).

Consider this  code fragment:

#include <vcc.h>

void requires_valid_ptr(char* ptr)
  _(requires \thread_local(ptr));

int someOffset(int n)
_(ensures \result >= 0 && \result < n) ;

int f(void)
{
  char a[10];

  int i = someOffset(10);
  requires_valid_ptr(&a[i]);
  requires_valid_ptr(&a[i-1]);
  requires_valid_ptr(&a[i+1]);
} 

VCC correctly finds  errors on the calls to require_valid_ptr() for &a[i-1] and &a[i+1]:

Verification of f failed. [0,69]
z:\edrdo\mpi\vcc\x.c(15,3) : error VC9502: Call 'requires_valid_ptr(&a[i-1])' did not verify.
z:\edrdo\mpi\vcc\x.c(4,14) : error VC9599: (related information) Precondition: '\thread_local(ptr)'.
z:\edrdo\mpi\vcc\x.c(16,3) : error VC9502: Call 'requires_valid_ptr(&a[i+1])' did not verify.
z:\edrdo\mpi\vcc\x.c(4,14) : error VC9599: (related information) Precondition: '\thread_local(ptr)'.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)

However if I use sizeof(a) rather than 10 in the call to someOffset(), vcc reports no errors.

Verification of f succeeded. [0,66]

Any C compiler will interpret sizeof(a) to be equal to 10 in this fragment. What's going on here? Maybe VCC is taking a to be a pointer to char rather than an array address? The  version information reported by VCC is :

Microsoft Research Vcc Version 2.3.426.0
Microsoft Research Boogie Version 2.1.40227.0
Microsoft Research Z3 Version Z3 version 3.2

Should I update it?

Thanks, best regards,

Eduardo Marques

VCC appears to understand sizeof() correctly as of 2.3.723.
I'm not sure it ever misunderstood it and I don't have the time to look at your code in detail right now, but I would advise you to update and try it out, just to check that you're not doing something wrong (like a pre or postcondition that implies false, for example).

Cheers,
Francois

[Quick Edit: I just tried with your code, and it goes through even with the current version. There is something wrong, either with VCC in this very special case, or with your example.]

[Solution: It appears that taking sizeof(a) makes VCC treat the array a in such a way that static allocation is unsound. Try sticking an _(assert \false) at the very beginning of f's body when using sizeof() on a and watch VCC succeed...]

#include <vcc.h>
int main(void)
{
  char a[10];
  _(assert sizeof(a) == 10)
  return 0;
}
`
Verification of main succeeded.
`

Hi,

Thanks, I tried your advice (update, assert \false, etc) ... the problem  persists with the latest version I just installed (2.3.724, just one revision ahead of the one you mentioned for correct sizeof() handling, I guess there's a reasonable chance that this is not yet too stable ...) 

To illustrate I consider two simple variations of your example below for the assertion "sizeof(a) > 10" (false, rather than sizeof(a) == 10). Both code snippets are equivalent, but the first one is handled correctly and the second is not.  The use of  _(assert \false) did not make any difference (and I didn't really understand from your explanation why it should ).

[Edit: Perhaps I need to update z3 and boogie as well?]

#include <vcc.h>
int main(void)
{
  char a[10];
  _(assert sizeof(a) > 10)
  return 0;
}
`
Verification of main failed. [0,59]
Z:\edrdo\mpi\vcc\z.c(7,12) : error VC9500: Assertion 'sizeof(a) > 10' did not verify.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)


#include <vcc.h>

int main(void)
{
  _(assert \false)
  char a[10];
  int n = sizeof(a);
  _(assert n > 10)

  return 0;
}
`
Verification of main succeeded. [0,72]

Sorry I was unclear: as I said, I didn't have much time to devote to this, and I was just thinking in writing and testing things out as I went.
The fact that the _(assert \false) does not cause a verification error (when it is obviously reachable, such as being at the very beginning of a function with no precondition) means that there is something very seriously wrong going on inside VCC and that you should file a bug report.

Maybe you could try reducing the example even further before filing the bug report, to help with identifying the actual issue.

In any case, there is nothing you're doing wrong: this is a VCC bug (the code below exercises all the border cases, feel free to use it when reporting the bug).
I have unfortunately no work-around to suggest.

Francois

#include <vcc.h>

// This one fails as it should
void good()
{
  _(assert \false)
  char a;
  int n = sizeof(a);
}

// This one succeeds, but shouldn't
int bad()
{
  _(assert \false)
  char a[10];
  return sizeof(a);
}

// This one fails as it should, which seems weird
void weird()
{
  char a[10];
  _(assert sizeof(a) != 10)
}

`
Verification of good failed.
testcase(6,12) : error VC9500: Assertion '\false' did not verify.
Verification of bad succeeded.
Verification of weird failed.
testcase(23,12) : error VC9500: Assertion 'sizeof(a) != 10' did not verify.
`

I submitted this to  the issue tracker then.

http://vcc.codeplex.com/workitem/6609

This issue is now fixed in the source repo. Thank you for reporting!