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

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