Ignore:
Timestamp:
Oct 7, 2011, 6:19:41 PM (8 years ago)
Author:
sacerdot
Message:
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1302 r1329  
    4040  Maybe there is a better way to organize the code!!! *)
    4141definition graph_succ_p: label → address → address.
    42  #l #_ generalize in match (refl … (beval_pair_of_pointer (pointer_of_label l)))
    43  cases (beval_pair_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
     42 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
     43 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    4444  [ #res #_ @res
    4545  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     
    5252   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    5353 λparams1,sem_params,globals,ge,st.
    54   (*CSC: the next two lines implement pointer_of_address;
    55     duplicated twice in joint/semantics.ma *)
    56   let 〈v1,v2〉 ≝ pc … st in
    57   do p ← pointer_of_bevals [v1;v2] ;
    58 
     54  do p ← pointer_of_address (pc … st) ;
    5955  let b ≝ pblock p in
    6056  do l ← label_of_pointer p;
Note: See TracChangeset for help on using the changeset viewer.