--- layout: fc_discuss_archives title: Message 7 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



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