Changeset 2508


Ignore:
Timestamp:
Nov 29, 2012, 8:12:34 PM (7 years ago)
Author:
mckinna
Message:

more tweaks. compiler and correctness still build.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2504 r2508  
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 (* moved to Fetch.ma *)
     329(* JHM: moved to Fetch.ma *)
    330330(* definition object_code ≝ list Byte. *)
    331331(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
  • src/common/StructuredTraces.ma

    r2503 r2508  
    5252qed.
    5353
    54 (* cost maps generalities *)
     54(* cost map generalities *)
    5555
    5656definition as_cost_labelled ≝
     
    7070
    7171definition as_cost_map ≝
    72   (* λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. *)
    7372  λS : abstract_status. (as_cost_label S) → ℕ.
    7473 
  • src/compiler.ma

    r2505 r2508  
    6666  λclight,code_memory,lbls,dec,k,asm_cost_map.
    6767  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    68     dec k asm_cost_map
    69   (*
    70    match dec asm_cost_map with
    71    [ inl prf ⇒ k «l_sig, prf»
    72    | inr _ ⇒ 0 (* labels not present in out code get 0 *)
    73    ]*).
     68    dec k asm_cost_map.
    7469
    7570include "ASM/ASMCostsSplit.ma".
    7671
    7772definition compile : clight_program →
    78   res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) (*(Σl.in_clight_program labelled l) → ℕ*)
     73  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled))
    7974λp.
    8075  ! 〈init_cost,p',p〉 ← front_end p;
Note: See TracChangeset for help on using the changeset viewer.