Changeset 2824 for src/ERTLptr


Ignore:
Timestamp:
Mar 8, 2013, 5:37:57 PM (7 years ago)
Author:
tranquil
Message:
  • moved sum on lists notation to extranat
  • used sum on lists to define portion of stack occupied by globals
  • corrected probable bug in joint semantics, where initial state would not move stack pointer past globals before setting up main
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2819 r2824  
    448448qed.
    449449
    450 definition first_free_stack_addr : ltl_program → nat ≝
    451  λp.
    452   let globals_addr_internal ≝
    453    λoffset : nat.
    454    λx_size: ident × region × nat.
    455     let 〈x, region, size〉 ≝ x_size in
    456      offset + size in
    457  foldl … globals_addr_internal 0 (prog_vars … p).
    458 
     450(* Paolo: does it really have sense to do here the first stack address computation,
     451   when it is an info easily available from any program in the back end?
     452   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
    459453definition ertlptr_to_ltl:
    460454 fixpoint_computer → coloured_graph_computer → ertlptr_program →
     
    462456  λthe_fixpoint,build,pr.
    463457   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    464    〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
     458   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
    465459%
    466460qed.
Note: See TracChangeset for help on using the changeset viewer.