# 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.

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

• Subject: [Frama-c-discuss] Proving the correctness of shifting operations
• From: michaelschausten at googlemail.com (Michael Schausten)
• Date: Thu, 17 Jun 2010 19:39:46 +0200

```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.
and some lemmas
(*Why axiom*) Lemma asr_positive_on_positive :
(forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> 0 <= (asr a b)))).

(*Why axiom*) Lemma asr_decreases_on_positive :
(forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> (asr a b) <= a))).

(*Why axiom*) Lemma asr_lsr_same_on_positive :
(forall (a:Z), (forall (b:Z), (0 <= a /\ 0 <= b -> (asr a b) =
(lsr a b)))).