| Copyright | (c) Galois Inc 2018 |
|---|---|
| License | BSD3 |
| Maintainer | Langston Barrett <lbarrett@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.LLVM.Errors
Contents
Description
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 Associated Types type Rep (LLVMSafetyAssertion sym) :: Type -> Type # Methods 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
Constructors
| 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 #