Changeset 496 for Deliverables/D3.1/Csemantics/Values.ma
 Timestamp:
 Feb 11, 2011, 4:45:28 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Values.ma
r487 r496 24 24 include "basics/logic.ma". 25 25 26 definition block ≝ Z. 27 (*definition eq_block ≝ zeq.*) 26 definition block ≝ region × Z. 27 28 definition eq_block ≝ 29 λb1,b2. 30 match b1 with [ pair r1 i1 ⇒ 31 match b2 with [ pair r2 i2 ⇒ 32 eq_region r1 r2 ∧ eqZb i1 i2 33 ] ]. 34 35 lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2. 36 (b1 = b2 → P true) → (b1 ≠ b2 → P false) → 37 P (eq_block b1 b2). 38 #P * #r1 #i1 * #r2 #i2 #H1 #H2 39 whd in ⊢ (?%) @eq_region_elim #H3 40 [ whd in ⊢ (?%) @eqZb_elim [ /2/  * #NE @H2 % #E @NE destruct % ] 41  @H2 % #E destruct elim H3 /2/ 42 ] qed. 28 43 29 44 (* * A value is either: … … 201 216 [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2) 202 217  Vptr pty2 b2 ofs2 ⇒ 203 if eq Zbb1 b2 then Vint (sub ofs1 ofs2) else Vundef218 if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef 204 219  _ ⇒ Vundef ] 205 220  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero  _ ⇒ Vundef ] … … 372 387  Vptr r1 b1 ofs1 ⇒ match v2 with 373 388 [ Vptr r2 b2 ofs2 ⇒ 374 if eq Zbb1 b2389 if eq_block b1 b2 375 390 then of_bool (cmp c ofs1 ofs2) 376 391 else cmp_mismatch c … … 391 406  Vptr r1 b1 ofs1 ⇒ match v2 with 392 407 [ Vptr r2 b2 ofs2 ⇒ 393 if eq Zbb1 b2408 if eq_block b1 b2 394 409 then of_bool (cmpu c ofs1 ofs2) 395 410 else cmp_mismatch c
Note: See TracChangeset
for help on using the changeset viewer.