CBMC malloc should fail if called for a size CBMC cannot represent

[danielsn]

I believe that CBMC can only represent allocations of size 2**(64-number-object-bits). And yet

    int *p = malloc(SIZE_MAX);
    assert(p);

succeeds. This should either return NULL, or block with an assume that the input to malloc is a representable size.

[xbauch]

@danielsn Now that #5210 was merged, this may be resolved. Please have a look at doc/cprover-manual/properties.md for description of the user-options that enable malloc to fail here.

[hannes-steffenhagen-diffblue]

THis has been implemented with the --malloc-may-fail and --malloc-fail-null flags.