--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2019 ---
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>