Use of malloc and free

Dec 17, 2012 at 1:58 PM
Edited Dec 17, 2012 at 1:59 PM

Hello,


I am having trouble understanding the verification of calls to malloc and free by VCC. Consider the following fragment:

 

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

char* foo() 
{
  char* p = (char*)malloc(10);
  if (p != NULL)
    free(p);
}

 

 

The output of vcc is as follows: 

 

e:\x.c(8,5) : error VC8510: Assertion '\extent(p) is writable in call to free(p)' did not verify.
e:\x.c(8,5) : error VC9502: Call 'free(p)' did not verify.
C:\Program Files\Microsoft Research\Vcc\Headers\Vcc3Prelude.bpl(1560,3) : error VC9599: (related information) Precondition: 'the extent of the object being reclaimed is mutable'.
C:\Program Files\Microsoft Research\Vcc\Headers\Vcc3Prelude.bpl(1562,3) : error VC9599: (related information) Precondition: 'the pointer being reclaimed was returned by malloc()'.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)

 

 

Is this a bug or do I need to specify annotations of some kind?

(Btw, how can I specify custom error messages for failed assertions as in free in the example above ? )

Thanks, best regards,

Eduardo

Developer
Dec 18, 2012 at 5:49 PM

Hi Eduardo,

You need to tell VCC what you are actually freeing, i.e. free(_(char[10]) p)

cheers, ernie

 

 

Dec 18, 2012 at 9:38 PM

Thanks a lot Ernie ...

PS: btw, I'd also be quite grateful if you provide a clue to http://vcc.codeplex.com/discussions/407075 :)

Mar 22, 2013 at 4:13 PM
Hello,

I have a similar issue to edrdo, but my issue is with int pointers. I do not understand the reason either of these do not verify:
int* foo() 
{
  int* p = (int*)malloc(10);
  if (p != NULL)
    free(_(int[10]) p);
}
or this:
int* foo() 
{
  int* p = (int*)malloc(sizeof(int*));
  if (p != NULL)
    free(_(int*) p);
}
Best,
Matt
Mar 24, 2013 at 10:51 PM
In the first case, the code is wrong. You probably meant int* p = (int*)malloc(10 * (sizeof(int)));. When you make this change (multiplying by (sizeof(int))), VCC verifies the code without issue.

The second example also has incorrect code, but when this is fixed (int** p = (int**)malloc(sizeof(int*));), I can not get VCC to verify it. Adding _(assume \writable(\extent(p))) before the call to free() results in the following error:
error VC0005: Argument '1': cannot convert from '\objset' to '\object'.
Is this a bug in VCC?