Changeset 1326 for src/RTL/semantics.ma

Timestamp:

Oct 7, 2011, 3:48:55 PM (9 years ago)

Author:

sacerdot

Message:

Code improved (now it uses the high level functions from joint/semantics.ma).

File:

• src/RTL/semantics.ma (modified) (1 diff)

src/RTL/semantics.ma

@@ -74 +74 @@
       let sp ≝ sp ? st in
       ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
-      ! regs ← reg_store dreg1 dpl (regs ? st) ;
-      ! regs ← reg_store dreg2 dph regs ;
-       ret ? 〈E0, goto … l (set_regs rtl_sem_params regs st)〉
+      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
+      ! st ← greg_store rtl_sem_params dreg2 dph st ;
+       ret ? 〈E0, goto … l st〉
    | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
    | rtl_st_ext_tailcall_id id regs ⇒ ?