Changeset 3037 for src/RTL/RTL.ma

Timestamp:

Mar 29, 2013, 5:19:53 PM (7 years ago)

Author:

tranquil

Message:

• ADDRESS joint instruction now has also an offset
• corrected call to pointer (needed to clear the accumulator)
• now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

File:

• src/RTL/RTL.ma (modified) (2 diffs)

src/RTL/RTL.ma

@@ -93 +93 @@
 
 (* parameters for main need to be passed to the premain *)
-definition RTL_premain : ∀p : rtl_program.joint_closed_internal_function RTL (prog_var_names ?? p) ≝
+definition RTL_premain : ∀p : rtl_program.
+  joint_closed_internal_function RTL (prog_names … p) ≝
 λp.
 let l1 : label ≝ an_identifier … one in
@@ -104 +105 @@
     an_identifier … (p0 (p0 one)) ] in
 let res ≝
-  mk_joint_internal_function RTL (prog_var_names … p)
+  mk_joint_internal_function RTL (prog_names … p)
   (mk_universe … (p0 (p0 one)))
   (mk_universe … (p1 (p0 one)))