Changeset 3062

Timestamp:

Apr 2, 2013, 11:59:02 AM (8 years ago)

Author:

sacerdot

Message:

Bug fixed in the semantics of Mov: the offset was ignored.
Now all tests pass.

Files:

• driver/tests/PROBLEMI (modified) (1 diff)
• extracted/interpret.ml (modified) (1 diff)
• src/ASM/Interpret.ma (modified) (1 diff)

driver/tests/PROBLEMI

@@ -4 +4 @@
 4. ok
 5. ok
-6. rotto chiamata puntatore (ma object code corretto!)
-7. rotto chiamata puntatore
+6. ok
+7. ok
 8. ok

extracted/interpret.ml

@@ -4313 +4313 @@
         Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
       in
-      let v = addr_of_symbol ident in
+      let v =
+        (Arithmetic.add_16_with_carry (addr_of_symbol ident) off Bool.False).Types.fst
+      in
       (match dst with
        | Types.Inl dptr -> Status.set_arg_16 cm s1 v dptr

src/ASM/Interpret.ma

@@ -1224 +1224 @@
     | Mov dst ident off ⇒
       let s ≝ set_clock ?? s (\fst ticks + clock … s) in
-      let v ≝ addr_of_symbol ident in
+      let v ≝ \fst (add_16_with_carry … (addr_of_symbol ident) off false) in
       match dst with
       [ inl dptr ⇒ set_arg_16 … s v dptr