Changeset 2674 for src/ERTLptr/ERTLptr.ma

Timestamp:

Feb 18, 2013, 5:48:19 PM (7 years ago)

Author:

tranquil

Message:

• another change in block definition
• RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken

File:

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

src/ERTLptr/ERTLptr.ma

@@ -20 +20 @@
     (* call_dest ≝ *) unit
     (* ext_seq ≝ *) ertlptr_seq
-    (* ext_seq_labels ≝ *) (λ_.[])
+    (* ext_seq_labels ≝ *)
+      (λs.match s with [ LOW_ADDRESS _ l ⇒ [l] | HIGH_ADDRESS _ l ⇒ [l] | _ ⇒ [ ]])
     (* has_tailcall ≝ *) false
     (* paramsT ≝ *) ℕ.