--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and unsigned int



Hi all,

I’m having some trouble proving assertion BAR below. The culprit seems to be the shift right operation — if I replace foo >> 8 with foo, then BAR is proven. Any pointers for making progress with minimal changes?

Thanks!
Alexander

#include <stdint.h>

typedef uint32_t Xuint32;

/*@ ensures x < y ==> \result == x;
    ensures x >= y ==> \result == y;
*/
Xuint32 MAX(Xuint32 x, Xuint32 y)
{
    if (x < y) {
        return x;
    }
    return y;
}

void bar(Xuint32 input) {
    Xuint32 foo = input;

    Xuint32 x1 = MAX(foo >> 8, 0xFFFF);
    Xuint32 x2 = MAX(foo, 0xFF);

    if (x1 + x2 < 128) {
        //@ assert BAR: x2 < 128;
    }
}

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191120/69e4a959/attachment.html>