CBMC does not warn when indexing off a void* #5275
Description
#include <assert.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <stdbool.h>
int main(int argc, char* argv[]) {
void* p = malloc(2);
void* q = &p[1];
printf("%p\n", p);
printf("%p\n", q);
return 0;
}
CBMC version: 5.12 (cbmc-5.12-104-g97993174d)
Operating system: OSX
Exact command line resulting in the issue:
cbmc --flush --bounds-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwind 1 --unwinding-assertions test.c
What behaviour did you expect: I expected it to say that you can't index using a void*, since void has no size
What happened instead:
** 0 of 49 failed (1 iterations)
VERIFICATION SUCCESSFUL