Malloc struct special treatment inconsistent with the general scenario.

[necto]

VeriFast seems to handle calls like malloc(sizeof(struct A)) specially, and generates the struct A-specific predicates right away for the successful allocation. On the other side malloc(size) generates just an array of chars, which, to be converted into the structure fields, requires additional assumptions regarding the structure layout. Specifically:

struct A {
  int x;
  int y;
};

int main ()
//@ requires true;
//@ ensures true;
{
  struct A* one = malloc(sizeof(struct A));
  if (one != NULL) one->y = 3;
  //@ assume(sizeof(struct A) == (sizeof(int) + sizeof(int)));
  struct A* two = malloc(1*sizeof(struct A));
  if (two != NULL) two->y = 3;
}

Here, first field assignments works, while the second case, first, requires the sizeof(struct A) == (sizeof(int) + sizeof(int)) for successful allocation, and then will also need assume((void*)&two->y == (void*)&two->x + sizeof(int)) to convert the generated chars into two fields A::x and A::y.

Long story short, for malloc(sizeof(struct A)) VeriFast silently assumes some layout facts, which it does not assume in the general case.

[btj]

I don't see that.

Note that for the malloc call to go through, it is sufficient to assume sizeof(struct A) <= INT_MAX.

To convert the chars chunk to the field chunks, the only assumption you really need is that the fields do not overlap and are within the range of the allocated block. In the example I gave earlier, I made specific layout assumptions only because this simplifies the conversion, not because it is necessary for the conversion.

[necto]

Agreed, the assumptions may be weaker.
But they still have to be made explicitly, while malloc(sizeof(struct A)) passes through without any.

[btj]

• The assume(sizeof(struct A) <= INT_MAX) will go away once we fix the parameter type of malloc.
• You can eliminate the other assumptions by using the close_struct(two); ghost command.