Queries.BlobSize returns the contents of a blob instead of its size

[mrstanb]

Description

I noticed that when calling Queries.BlobSize on a pointer, containing dynamically-allocated memory, BlobSize returns the contents of the blob that the pointer points to instead of the blob's size.

Take the following C program as an example:

#include <stdlib.h>

int main(int argc, char const *argv[]) {
    char *ptr = malloc(5 * sizeof(char));

    *ptr = 'a';

    free(ptr); //BlobSize

    return 0;
}

Observed Behavior

Calling BlobSize for ptr in the program above for the line with the comment //BlobSize returns the contents of ptr's blob, namely 97 (i.e., the char a in decimal ASCII encoding).

Expected Behavior

Calling BlobSize for ptr in the program above for the line with the comment //BlobSize should return 5, since ptr points to a heap memory block with size 5 * sizeof(char) which should evaluate to 5

Further remarks

I noticed that in the match in base.ml's query function here, the second match case is always taken, i.e., BlobSize always gives back top and never matches the Blob (_,s,_) case.

[sim642]

Nothing right now uses BlobSize, so it's not surprising that it broke at one point when modifying the blob domain.