Ignore:
Timestamp:
Mar 8, 2013, 3:51:18 PM (7 years ago)
Author:
tranquil
Message:
  • corrected bug in ERTL semantics (both delframe and newframe did the same operation on the stack pointer...)
  • split RTL semantics in two (one with multiple stack spaces per call, one with only one for all)
  • joint_if_entry is not required anymore to be in the code (as it is covered by entry_costed in good_if)
  • temporarily replaced the two biggest proofs of linearise by daemons
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2808 r2823  
    502502; ss_def_out_eq :
    503503           joint_if_stacksize … def_out = init_stack_size … data
    504 ; entry_eq :
    505           pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in)
     504; entry_eq : joint_if_entry … def_out = joint_if_entry … def_in
    506505; partition_lbls : partial_partition … f_lbls
    507506; partition_regs : partial_partition … f_regs
     
    573572    (joint_if_local_stacksize … def)
    574573    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
    575     («pi1 … entry, mem_set_add_id …») in
     574    entry in
    576575  let f : label → joint_statement (src_g_pars : params) globals →
    577576    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
Note: See TracChangeset for help on using the changeset viewer.