Copyright | (c) Galois Inc 2018 |
---|---|
License | BSD3 |
Maintainer | Langston Barrett <lbarrett@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data LLVMSafetyAssertion sym
- data BadBehavior sym where
- BBUndefinedBehavior :: UndefinedBehavior (RegValue' sym) -> BadBehavior sym
- BBMemoryError :: MemoryError sym -> BadBehavior sym
- undefinedBehavior :: UndefinedBehavior (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym
- undefinedBehavior' :: UndefinedBehavior (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym
- poison :: Poison (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym
- poison' :: Poison (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym
- memoryError :: 1 <= w => MemoryOp sym w -> MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
- detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
- explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
- ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
- concBadBehavior :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym)
- classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym)
- predicate :: Simple Lens (LLVMSafetyAssertion sym) (Pred sym)
- extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)
Documentation
data LLVMSafetyAssertion sym Source #
Instances
Generic (LLVMSafetyAssertion sym) Source # | |
Defined in Lang.Crucible.LLVM.Errors type Rep (LLVMSafetyAssertion sym) :: Type -> Type # from :: LLVMSafetyAssertion sym -> Rep (LLVMSafetyAssertion sym) x # to :: Rep (LLVMSafetyAssertion sym) x -> LLVMSafetyAssertion sym # | |
type Rep (LLVMSafetyAssertion sym) Source # | |
Defined in Lang.Crucible.LLVM.Errors type Rep (LLVMSafetyAssertion sym) = D1 ('MetaData "LLVMSafetyAssertion" "Lang.Crucible.LLVM.Errors" "crucible-llvm-0.6-JJ7tfvbGrbFFTkl5eJBN3H" 'False) (C1 ('MetaCons "LLVMSafetyAssertion" 'PrefixI 'True) (S1 ('MetaSel ('Just "_classifier") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BadBehavior sym)) :*: (S1 ('MetaSel ('Just "_predicate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pred sym)) :*: S1 ('MetaSel ('Just "_extra") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))) |
data BadBehavior sym where Source #
Combine the three types of bad behaviors
BBUndefinedBehavior :: UndefinedBehavior (RegValue' sym) -> BadBehavior sym | |
BBMemoryError :: MemoryError sym -> BadBehavior sym |
undefinedBehavior :: UndefinedBehavior (RegValue' sym) -> Pred sym -> LLVMSafetyAssertion sym Source #
undefinedBehavior' :: UndefinedBehavior (RegValue' sym) -> Pred sym -> Text -> LLVMSafetyAssertion sym Source #
memoryError :: 1 <= w => MemoryOp sym w -> MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym Source #
concBadBehavior :: IsExprBuilder sym => sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> BadBehavior sym -> IO (BadBehavior sym) Source #
Lenses
classifier :: Simple Lens (LLVMSafetyAssertion sym) (BadBehavior sym) Source #