Changeset 2952 for src/RTL/RTL.ma


Ignore:
Timestamp:
Mar 26, 2013, 2:01:15 PM (7 years ago)
Author:
tranquil
Message:
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2946 r2952  
    113113  res in
    114114let res ≝ add_graph … l2
    115   (sequential … (CALL RTL ? (inl … (prog_main … p)) (map … (Reg ?) rs) rs) l3)
     115  (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] l3)
    116116  res in
    117117let res ≝ add_graph … l3
Note: See TracChangeset for help on using the changeset viewer.