--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on June 2010 ---
Hello, I have the following piece of code, which I'd like to prove in Coq: int test = 29; int test2 = 1 << test; This gives me 3 VCs: - test >= 0 - test < 32 (both are easily proved by intuition) - 1 <= asr(2147483647, test) I first tried to prove the 3rd VC with alt-ergo, which didn't succeed. In Coq, I have the same problem. "asr" should probably stand for arithmetic shift right, so in the end it's about sth. like "1 <= 4". However, 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 (*Why axiom*) Lemma asr_positive_on_positive : (forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> 0 <= (asr a b)))). Admitted. (*Why axiom*) Lemma asr_decreases_on_positive : (forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> (asr a b) <= a))). Admitted. (*Why axiom*) Lemma asr_lsr_same_on_positive : (forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> (asr a b) = (lsr a b)))). Admitted. I don't know how to prove the shift now. 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. Regards, Michael