Changeset 2999 for src/correctness.ma


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/correctness.ma

    r2928 r2999  
    100100definition simulates ≝
    101101  λp: compiler_output.
    102   let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
     102  let initial_status ≝ initialise_status … (cm c_labelled_object_code … p) in
    103103  ∀m1,m2.
    104104   measurable Clight_pcs (c_labelled_clight … p) m1 m2
Note: See TracChangeset for help on using the changeset viewer.