--- layout: fc_discuss_archives title: Message 37 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,

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