As array and NULL pointers in /3

Aug 25, 2011 at 1:01 PM

Hi all,

I have been switching to VCC3, and have found that a couple of my previously verifying programs stopped verifying because of something I personally find weird: assuming that a pointer is typed as an array does not seem to guarantee that its address is not NULL.

For example, the following fails on the _(assert ptr != NULL):

#include <vcc.h>
#include <stdlib.h>

void test(char* ptr)
  _(requires \mutable((char[4]) ptr))
{ _(assert ptr != NULL) }

Is this a bug, and if not, what is the rationale behind it?