Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Simulator.PathSatisfiability

Description

Synopsis

checkPathSatisfiability :: ConfigOption BaseBoolType
pathSatisfiabilityFeature :: forall sym. IsSymInterface sym => sym -> (Maybe ProgramLoc -> Pred sym -> IO BranchResult) -> IO (GenericExecutionFeature sym)
checkSatToConsiderBranch :: IsSymInterface sym => sym -> (Pred sym -> IO (SatResult () ())) -> Pred sym -> IO BranchResult
data BranchResult

Documentation

checkPathSatisfiability :: ConfigOption BaseBoolType Source #

pathSatisfiabilityFeature Source #

Arguments

:: forall sym. IsSymInterface sym
=> sym
-> (Maybe ProgramLoc -> Pred sym -> IO BranchResult)	An action for considering the satisfiability of a predicate. In the current state of the symbolic interface, indicate what we can determine about the given predicate.
-> IO (GenericExecutionFeature sym)

checkSatToConsiderBranch :: IsSymInterface sym => sym -> (Pred sym -> IO (SatResult () ())) -> Pred sym -> IO BranchResult Source #

data BranchResult Source #

Result of attempting to branch on a predicate.

Constructors

IndeterminateBranchResult	The both branches of the predicate might be satisfiable (although satisfiablility of either branch is not guaranteed).
NoBranch !Bool	Commit to the branch where the given predicate is equal to the returned boolean. The opposite branch is unsatisfiable (although the given branch is not necessarily satisfiable).
UnsatisfiableContext	The context before considering the given predicate was already unsatisfiable.

Instances

Instances details

Data BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BranchResult -> c BranchResult # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BranchResult # toConstr :: BranchResult -> Constr # dataTypeOf :: BranchResult -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BranchResult) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BranchResult) # gmapT :: (forall b. Data b => b -> b) -> BranchResult -> BranchResult # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BranchResult -> r # gmapQ :: (forall d. Data d => d -> u) -> BranchResult -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BranchResult -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult #
Generic BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Associated Types type Rep BranchResult :: Type -> Type # Methods from :: BranchResult -> Rep BranchResult x # to :: Rep BranchResult x -> BranchResult #
Eq BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods (==) :: BranchResult -> BranchResult -> Bool # (/=) :: BranchResult -> BranchResult -> Bool #
Ord BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online Methods compare :: BranchResult -> BranchResult -> Ordering # (<) :: BranchResult -> BranchResult -> Bool # (<=) :: BranchResult -> BranchResult -> Bool # (>) :: BranchResult -> BranchResult -> Bool # (>=) :: BranchResult -> BranchResult -> Bool # max :: BranchResult -> BranchResult -> BranchResult # min :: BranchResult -> BranchResult -> BranchResult #
type Rep BranchResult Source #
Instance details Defined in Lang.Crucible.Backend.Online type Rep BranchResult = D1 ('MetaData "BranchResult" "Lang.Crucible.Backend.Online" "crucible-0.7-8cOLouRuT7vG1hxVUUUvCh" 'False) (C1 ('MetaCons "IndeterminateBranchResult" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NoBranch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :+: C1 ('MetaCons "UnsatisfiableContext" 'PrefixI 'False) (U1 :: Type -> Type)))