Changeset 2899 for src/compiler.ma


Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (7 years ago)
Author:
sacerdot
Message:
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2875 r2899  
    5151  | ltl_pass ⇒ with_stack_model ltl_program
    5252  | lin_pass ⇒ with_stack_model lin_program
    53   | assembly_pass ⇒ pseudo_assembly_program
     53  | assembly_pass ⇒
     54     pseudo_assembly_program × (Word → Word) × (Word → bool)
    5455  | object_code_pass ⇒ labelled_object_code ].
    5556
     
    114115  let i ≝ observe lin_pass 〈p,st〉 in
    115116   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    116   let i ≝ observe assembly_pass p in
    117117   return 〈p,stack_cost,max_stack〉.
    118118
     
    126126  let sigma ≝ λppc. \fst sigma_pol ppc in
    127127  let pol ≝ λppc. \snd sigma_pol ppc in
     128  let i ≝ observe assembly_pass 〈p,sigma,pol〉 in
    128129  let p ≝ assembly p sigma pol in
    129130  let i ≝ observe object_code_pass p in
     
    135136definition lift_cost_map_back_to_front :
    136137  ∀clight, code_memory, lbls.
    137     let abstat ≝ ASM_abstract_status code_memory lbls in
     138    let abstat ≝ OC_abstract_status code_memory lbls in
    138139  as_cost_map abstat → clight_cost_map clight ≝
    139140  λclight,code_memory,lbls,k,asm_cost_map.
Note: See TracChangeset for help on using the changeset viewer.