Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1416 r1451  
    3434  pointer arithmetics on Code pointers.
    3535*)
    36 definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
    37  λl.
     36definition graph_pointer_of_label0:
     37 pointer → label → Σp:pointer. ptype p = Code ≝
     38 λoldpc,l.
    3839  mk_pointer Code
    3940   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
     
    4142// qed.
    4243
     44definition graph_pointer_of_label:
     45 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
     46 λ_.λ_.λ_.λoldpc,l.
     47  OK ? (graph_pointer_of_label0 oldpc l).
     48
    4349(*CSC: XXXX; inverse of the previous function, but it does not check that
    4450  the offset is zero and thus it never fails. *)
    45 definition label_of_pointer: pointer → res label ≝
     51definition graph_label_of_pointer: pointer → res label ≝
    4652 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
    4753
     
    5258 to organize the code? *)
    5359definition graph_succ_p: label → address → res address ≝
    54  λl.λ_.address_of_pointer (pointer_of_label l).
     60 λl,old.
     61  do ptr ← pointer_of_address old ;
     62  let newptr ≝ graph_pointer_of_label0 ptr l in
     63  address_of_pointer newptr.
    5564
    5665axiom BadProgramCounter: String.
     
    7584  do p ← code_pointer_of_address (pc … st) ;
    7685  do f ← graph_fetch_function … ge st ;
    77   do l ← label_of_pointer p;
     86  do l ← graph_label_of_pointer p;
    7887  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracChangeset for help on using the changeset viewer.