--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on November 2019 ---
ons 2019-11-20 klockan 15:58 -0800 skrev Alexander Bakst: > 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); Maybe add some @asserts for the ranges of x1 and x2 here? > > if (x1 + x2 < 128) { The prover might suspect x1 + x2 might overflow here, unless you hold its hand (adding the asserts above) > //@ assert BAR: x2 < 128; > } > } /Tomas