Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_LTL_LIN_semantics.ml

    r3019 r3043  
    209209  | Joint_semantics.PTR ->
    210210    Obj.magic
    211       (Monad.m_return0 (Monad.max_def Errors.res0)
    212         st.Joint_semantics.st_no_pc)
     211      (Monad.m_bind0 (Monad.max_def Errors.res0)
     212        (Obj.magic
     213          (ByteValues.byte_of_val ErrorMessages.BadFunction
     214            (SemanticsUtils.hwreg_retrieve
     215              (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs)
     216              I8051.RegisterA))) (fun v ->
     217        match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     218                (Nat.S (Nat.S Nat.O)))))))) v
     219                (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     220                  (Nat.S (Nat.S Nat.O))))))))) with
     221        | Bool.True ->
     222          Monad.m_return0 (Monad.max_def Errors.res0)
     223            st.Joint_semantics.st_no_pc
     224        | Bool.False ->
     225          Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     226            ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
     227            ErrorMessages.BadPointer), List.Nil)))))))
    213228  | Joint_semantics.ID ->
    214229    Joint_semantics.push_ra lTL_LIN_state st.Joint_semantics.st_no_pc
Note: See TracChangeset for help on using the changeset viewer.