Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (7 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2907 r2999  
    316316definition ASM_cost_map :
    317317  ∀p: labelled_object_code.
    318   let code_memory ≝ load_code_memory (oc p) in
    319318  let a_s ≝ OC_abstract_status p in
    320319  as_cost_map a_s ≝
Note: See TracChangeset for help on using the changeset viewer.