Changeset 2909 for extracted/compiler.ml
 Timestamp:
 Mar 19, 2013, 10:21:08 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/compiler.ml
r2905 r2909 601 601 602 602 (** val lift_cost_map_back_to_front : 603 Csyntax.clight_program > BitVector.byte BitVectorTrie.bitVectorTrie > 604 CostLabel.costlabel BitVectorTrie.bitVectorTrie > 603 Csyntax.clight_program > ASM.labelled_object_code > 605 604 StructuredTraces.as_cost_map > Label.clight_cost_map **) 606 let lift_cost_map_back_to_front clight code_memory lblsk asm_cost_map =605 let lift_cost_map_back_to_front clight oc k asm_cost_map = 607 606 StructuredTraces.lift_sigma_map_id Nat.O 608 607 (BitVectorTrie.strong_decidable_in_codomain 609 608 (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S 610 609 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 611 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))612 (Obj.magic k) (Obj.magic asm_cost_map)610 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) 611 (Obj.magic oc.ASM.costlabels)) (Obj.magic k) (Obj.magic asm_cost_map) 613 612 614 613 open UtilBranch … … 777 776 Monad.m_bind0 (Monad.max_def Errors.res0) 778 777 (Obj.magic (assembler observe p1)) (fun p2 > 779 prerr_endline "COMPUTE_COST_MAP";780 778 let k = ASMCostsSplit.aSM_cost_map p2 in 781 prerr_endline "LIFT_COST_MAP"; 782 let k' = 783 lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc) 784 p2.ASM.costlabels k 785 in 786 prerr_endline "END"; 779 let k' = lift_cost_map_back_to_front p' p2 k in 787 780 Monad.m_return0 (Monad.max_def Errors.res0) 788 781 { c_labelled_object_code = p2; c_stack_cost = stack_cost;
Note: See TracChangeset
for help on using the changeset viewer.