{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator
(
RegValue
, RegValue'(..)
, VariantBranch(..)
, injectVariant
, AnyValue(..)
, FnVal(..)
, fnValType
, RolledType(..)
, RegEntry(..)
, RegMap(..)
, emptyRegMap
, regVal
, assignReg
, reg
, SimErrorReason(..)
, SimError(..)
, ppSimError
, GlobalVar(..)
, SymGlobalState
, emptyGlobals
, GlobalPair(..)
, gpValue
, gpGlobals
, AbortedResult(..)
, PartialResult(..)
, partialValue
, ExecResult(..)
, ExecState(..)
, ExecCont
, execResultContext
, Override(..)
, FnState(..)
, FunctionBindings(..)
, ExtensionImpl(..)
, EvalStmtFunc
, emptyExtensionImpl
, IsSymInterfaceProof
, SimContext(..)
, initSimContext
, ctxSymInterface
, functionBindings
, cruciblePersonality
, profilingMetrics
, SimState
, initSimState
, defaultAbortHandler
, AbortHandler(..)
, CrucibleState
, stateContext
, IntrinsicClass
, IntrinsicMuxFn(..)
, IntrinsicTypes
, emptyIntrinsicTypes
, executeCrucible
, singleStepCrucible
, evalReg
, evalArgs
, stepStmt
, stepTerm
, stepBasicBlock
, ExecutionFeature
, GenericExecutionFeature
, genericToExecutionFeature
, timeoutFeature
, module Lang.Crucible.Simulator.OverrideSim
) where
import Lang.Crucible.CFG.Common
import Lang.Crucible.Simulator.ExecutionTree
import Lang.Crucible.Simulator.EvalStmt
import Lang.Crucible.Simulator.GlobalState
import Lang.Crucible.Simulator.Intrinsics
import Lang.Crucible.Simulator.Operations
import Lang.Crucible.Simulator.OverrideSim
import Lang.Crucible.Simulator.RegMap
import Lang.Crucible.Simulator.SimError