diff --git a/deps/macaw b/deps/macaw index ad51ae3c54..a43151963d 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit ad51ae3c54be97f4f7d15e8eaed9344341ce88e4 +Subproject commit a43151963da70e4d4c3d69f9605e82e44ff30731 diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 578d2cbf35..ce90faef4b 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -185,7 +185,7 @@ data Fun = Fun { funName :: ByteString, funSpec :: FunSpec } -------------------------------------------------------------------------------- -type CallHandler = Sym -> Macaw.LookupFunctionHandle Sym X86_64 +type CallHandler = Sym -> Macaw.LookupFunctionHandle (MacawSimulatorState Sym) Sym X86_64 -- | Run a top-level proof. -- Should be used when making a standalone proof script. diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index f160e6bc00..d11e3ef2ae 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -123,7 +123,10 @@ import Lang.Crucible.Types import Verifier.SAW.SharedTerm (Term,scApplyAll,scVector,scBitvector,scAt,scNat) import Data.Macaw.Memory(RegionIndex) -import Data.Macaw.Symbolic(GlobalMap(..), ToCrucibleType, LookupFunctionHandle(..), MacawCrucibleRegTypes) +import Data.Macaw.Symbolic + ( GlobalMap(..), ToCrucibleType, LookupFunctionHandle(..) + , MacawCrucibleRegTypes, MacawSimulatorState + ) import Data.Macaw.Symbolic.Backend ( crucArchRegTypes ) import Data.Macaw.X86.X86Reg import Data.Macaw.X86.Symbolic @@ -1203,7 +1206,7 @@ _debugDumpGoals opts = sh (ProofGoal _hyps g) = print (view labeledPredMsg g) -type Overrides = Map (Natural,Integer) (Sym -> LookupFunctionHandle Sym X86_64) +type Overrides = Map (Natural,Integer) (Sym -> LookupFunctionHandle (MacawSimulatorState Sym) Sym X86_64) -- | Use a specification to verify a function. -- Returns the initial state for the function, and a post-condition.