Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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