Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2823 r2946  
    885885   ≝
    886886  λp,pr.transform_program ??? pr
    887     (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
     887    mk_joint_program
     888      (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))
     889      (init_cost_label … pr).
    888890
    889891(*
Note: See TracChangeset for help on using the changeset viewer.