Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (8 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1384 r1385  
    5454
    5555axiom BadProgramCounter: String.
     56
     57definition graph_fetch_function:
     58 ∀params1,sem_params,globals.
     59  genv … (graph_params params1 globals) →
     60   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
     61 λparams1,sem_params,globals,ge,st.
     62  do p ← pointer_of_address (pc … st) ;
     63  let b ≝ pblock p in
     64  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     65  match def with
     66  [ Internal def' ⇒ OK … def'
     67  | External _ ⇒ Error … [MSG BadProgramCounter]].
     68
    5669definition graph_fetch_statement:
    5770 ∀params1,sem_params,globals.
     
    6073 λparams1,sem_params,globals,ge,st.
    6174  do p ← pointer_of_address (pc … st) ;
    62   let b ≝ pblock p in
    63   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    64   match def with
    65   [ Internal def' ⇒
    66      do l ← label_of_pointer p;
    67      opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
    68   | External _ ⇒ Error … [MSG BadProgramCounter]].
     75  do f ← graph_fetch_function … ge st ;
     76  do l ← label_of_pointer p;
     77  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracChangeset for help on using the changeset viewer.