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/Globalenvs.ma

    r496 r498  
    341341definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝
    342342λF,name_fun,g.
    343   let b ≝ nextfunction ? g in
    344   mk_genv F ((*ZMap.set*) λb'. if eq_block 〈Code,b〉 b' then (Some ? (\snd name_fun)) else (functions ? g b'))
    345             (Zpred b)
    346             ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
     343  let blk_id ≝ nextfunction ? g in
     344  let b ≝ mk_block Code blk_id in
     345  mk_genv F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
     346            (Zpred blk_id)
     347            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? g i) ]).
    347348
    348349definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝
     
    403404     addresses of the memory region in question - here there are no real
    404405     pointers, so use the real region. *)
    405   let r ≝ \fst b in
     406  let r ≝ block_region m b in
    406407  match id with
    407408  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     
    468469definition alloc_init_data : mem → list init_data → region → mem × block ≝
    469470  λm,i_data,r.
    470   〈mk_mem (update_block ? 〈r, nextblock m〉
     471  let b ≝ mk_block r (nextblock m) in
     472  〈mk_mem (update_block ? b
    471473                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    472474                 (blocks m))
    473475         (Zsucc (nextblock m))
    474476         (succ_nextblock_pos m),
    475    〈r, nextblock m〉〉.
     477   b〉.
    476478
    477479(* init *)
Note: See TracChangeset for help on using the changeset viewer.