Changeset 2952 for src/LIN/LIN.ma

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:

• src/LIN/LIN.ma (modified) (1 diff)

src/LIN/LIN.ma

@@ -34 +34 @@
 let code ≝
   [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
-   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4 it) it〉 ;
+   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
    〈Some ? l3, GOTO ? l3〉 ] in
 mk_joint_internal_function LIN (prog_var_names … p)