Strange type mismatch in malloc

[jameshfisher]

Take the following program:

#include <stdlib.h> /* malloc */

void foo()
//@ requires true;
//@ ensures true;
{
  unsigned int count = 3;
  malloc(sizeof(unsigned char) * count);
}

After applying my patch in #28 and running VeriFast, i get the error:

foo.c(8,34-39): Type mismatch. Actual: uintptr_t. Expected: int.

The IDE highlights count as the source of the type error. I don't know where the int expectation is coming from.

I don't understand why, if I pull out the expression into its own variable, VeriFast passes:

#include <stdlib.h> /* malloc */
#include <stddef.h> /* size_t */

void foo()
//@ requires true;
//@ ensures true;
{
  unsigned int count = 3;
  size_t size = sizeof(unsigned char) * count;
  malloc(size);
}

[btj]

VeriFast treats expressions of the form malloc(sizeof(T) * E) or malloc(E * sizeof(T)) specially, to generate the appropriate typed array chunk (like ints) declared in prelude.h. Currently, it typechecks E against type int. See https://github.com/verifast/verifast/blob/master/src/verify_expr.ml#L1818.

I guess it should instead typecheck E against type size_t.

[jameshfisher]

Ah, that would explain it. I'm not sure what E should typecheck as. I think there are many valid types. My intuition is that a size_t multiplied by any natural number should yield another size_t, so E just has to be integral and non-negative. But this depends on C's type conversion rules, which I'm not very familiar with.