--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on June 2010 ---
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