Skip to content

Why is explicit (size_t) casting required on byte_counts(unsigned _)? #545

@AnnaKornfeldSimpson

Description

@AnnaKornfeldSimpson

In the following code snippet, why am I required to explicitly cast freespace to a size_t when defining the bounds for the args to memcpy? If I do not, it gives me a cannot prove bounds warning where the only difference between expected and inferred bounds is that the expected bounds have a (size_t) cast in front of freespace. freespace is already unsigned, it should be able to implicitly convert to size_t. The same behavior occurs when the length is a uint32_t instead of an unsigned int.

foo(uint8_t *buf : itype(array_ptr<uint8_t>) byte_count(len), const uint8_t *data : itype(array_ptr<uint8_t>) byte_count(len), size_t len) {
    unsigned int freespace = TOTAL - USED;
    if (len >= freespace) {
        array_ptr<uint8_t> midBuffer : byte_count((size_t)freespace) = 
            dynamic_bounds_cast<array_ptr<uint8_t>>(buf, byte_count((size_t)freespace));
        // identical dynamic cast for data to tmpData omitted
        memcpy(midBuffer, tmpData, freespace);
    }
}

Note: This bug definitely occurs on Linux and I'm pretty sure also on Windows. Both should be using 64-bit versions of checkedc-clang.

Metadata

Metadata

Assignees

No one assigned

    Labels

    priority:3This labels bugs that are not very critical but still need to be addressed.work itemThis labels issues that are not exactly bugs but are about improvements.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions