Symbiotic does not check the size of memory returned by malloc

[jamartis]

#include <stdlib.h>
int main()
{
    void *mem = malloc(sizeof(mem));
    void **ok = mem;

    mem = malloc(sizeof(mem));
    char *warn = mem;

    mem = malloc(sizeof(char));
    void **err = mem;

    *err = NULL;

    free (ok);
    free (warn);
    free (err);
    return 0;
}

The code above contains an error on the line *err = NULL (the err has been malloced to the sizeof(char), and is being assigned a pointer). Symbiotic however does not report an error.

This may be related to this warning issued by symbiotic:

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.

symbiotic --version version: 6.1.0-dev

[mchalupa]

Yes, I am able to reproduce this one. KLEE does not find any error not even on the original file without any optimizations and slicing, so the problem should be in KLEE, probably due to the warning you mentioned.