Ignore:
Timestamp:
Feb 11, 2011, 4:45:36 PM (9 years ago)
Author:
campbell
Message:

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Values.ma

    r496 r498  
    2424include "basics/logic.ma".
    2525
    26 definition block ≝ region × Z.
     26record block : Type[0] ≝
     27{ block_region : region
     28; block_id : Z
     29}.
    2730
    2831definition eq_block ≝
    2932λ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 ] ].
     33  eq_region (block_region b1) (block_region b2) ∧
     34  eqZb (block_id b1) (block_id b2)
     35.
    3436
    3537lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
Note: See TracChangeset for help on using the changeset viewer.