--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving the correctness of shifting operations



Hello,

> - 1 <= asr(2147483647, test)
>
> I first tried to prove the [above] VC with alt-ergo, which didn't succeed. In
> Coq, I have the same problem.

This verification condition expresses that "1<<test" does
not result in an overflow. An overflow could make the
underlying 2's complement representation visible by changing
the sign bit, or any other behavior: it's undefined as per
section 6.5.8, paragraph 4, of the C99 standard.

It looks a bit contrived as a way to express this condition,
but it is in fact the simplest way, assuming that you can
rely on the asr function in the logic.

> I couldn't find any sort of declaration of asr in the coq-file.
> There's only a
> ? (*Why logic*) Definition asr : Z -> Z -> Z.
> ? Admitted.
> and some lemmas

It appears that both in Alt-Ergo and in Coq outputs, asr is partially
axiomatized. In Coq, you can remedy the situation by providing
more axioms. In particular, axioms that express:

- if x >= 2, then (asr x 1) >= 1

- if x, y, z are positive, then (asr (asr x y) z) = asr x (y+z)

may be enough, and they may even be sound (no guarantees though,
I am a specialist of providing unsound axiomatizations).

> I also found out that, if i change
> the code to "int test2 = 1 << 29" (leaving out the variable), there's no VC
> created at all.

That's because of a constant propagation applied during parsing.
In this case Jessie does not even see the "<<" operation.

Best regards,

Pascal