Ignore:
Timestamp:
Mar 5, 2013, 6:15:06 PM (8 years ago)
Author:
sacerdot
Message:
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2739 r2774  
    443443qed.
    444444
     445definition first_free_stack_addr : ltl_program → nat ≝
     446 λp.
     447  let globals_addr_internal ≝
     448   λoffset : nat.
     449   λx_size: ident × region × nat.
     450    let 〈x, region, size〉 ≝ x_size in
     451     offset + size in
     452 foldl … globals_addr_internal 0 (prog_vars … p).
     453
    445454definition ertlptr_to_ltl:
    446  fixpoint_computer → coloured_graph_computer → ertlptr_program → ltl_program ≝
    447   λthe_fixpoint,build.
    448    b_graph_transform_program … (translate_data the_fixpoint build).
     455 fixpoint_computer → coloured_graph_computer → ertlptr_program →
     456  ltl_program × stack_cost_model × nat ≝
     457  λthe_fixpoint,build,pr.
     458   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
     459   〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
Note: See TracChangeset for help on using the changeset viewer.