Changeset 2823 for src/RTLabs


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/RTLabs/RTLabsToRTL.ma

    r2808 r2823  
    10341034  let luniverse' ≝ f_labgen def in
    10351035  let stack_size' ≝ f_stacksize def in
    1036   let entry' ≝ f_entry def in
     1036  let entry' ≝ pi1 … (f_entry def) in
    10371037  let init ≝ mk_joint_internal_function RTL globals
    10381038    luniverse' runiverse' [ ] [ ] stack_size' stack_size'
    1039     (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
     1039    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10401040  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
    10411041    (f_locals def) (f_params def) (f_result def) init in
     
    10491049    ] (dpi2 … pr) in
    10501050  foldi … f_trans (f_graph def) init'.
    1051 [4: >graph_code_has_point @mem_set_add_id ] 
    10521051(* TODO *) cases daemon
    10531052qed.
Note: See TracChangeset for help on using the changeset viewer.