Changeset 1153 for Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

Timestamp:

Aug 30, 2011, 6:55:12 PM (10 years ago)

Author:

campbell

Message:

Merge trunk into branch.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• ERTL/ERTL.ma (modified) (2 diffs)

Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

@@ -20 +20 @@
   | ertl_st_pop: register → label → ertl_statement
   | ertl_st_push: register → label → ertl_statement
+  | ertl_st_addr: register → register → ident → label → ertl_statement
+(* XXX: changed from O'Caml
   | ertl_st_addr_h: register → ident → label → ertl_statement
   | ertl_st_addr_l: register → ident → label → ertl_statement
+*)
   | ertl_st_int: register → Byte → label → ertl_statement
   | ertl_st_move: register → register → label → ertl_statement
+  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
+(* XXX: changed from O'Caml
   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
+*)
   | ertl_st_op1: Op1 → register → register → label → ertl_statement
   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
@@ -32 +38 @@
   | ertl_st_load: register → register → register → label → ertl_statement
   | ertl_st_store: register → register → register → label → ertl_statement
-  | ertl_st_call_id: ident → Byte → label → ertl_statement
+  | ertl_st_call_id: ident → nat → label → ertl_statement
   | ertl_st_cond: register → label → label → ertl_statement
   | ertl_st_return: ertl_statement.