Changeset 3062


Ignore:
Timestamp:
Apr 2, 2013, 11:59:02 AM (4 years ago)
Author:
sacerdot
Message:

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

Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/tests/PROBLEMI

    r3058 r3062  
    444. ok
    555. ok
    6 6. rotto chiamata puntatore (ma object code corretto!)
    7 7. rotto chiamata puntatore
     66. ok
     77. ok
    888. ok
  • extracted/interpret.ml

    r3060 r3062  
    43134313        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    43144314      in
    4315       let v = addr_of_symbol ident in
     4315      let v =
     4316        (Arithmetic.add_16_with_carry (addr_of_symbol ident) off Bool.False).Types.fst
     4317      in
    43164318      (match dst with
    43174319       | Types.Inl dptr -> Status.set_arg_16 cm s1 v dptr
  • src/ASM/Interpret.ma

    r3060 r3062  
    12241224    | Mov dst ident off ⇒
    12251225      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1226       let v ≝ addr_of_symbol ident in
     1226      let v ≝ \fst (add_16_with_carry … (addr_of_symbol ident) off false) in
    12271227      match dst with
    12281228      [ inl dptr ⇒ set_arg_16 … s v dptr
Note: See TracChangeset for help on using the changeset viewer.