crucible-llvm-0.10: Support for translating and executing LLVM code in Crucible

Copyright	(c) Galois Inc 2026
License	BSD3
Maintainer	Langston Barrett <langston@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.LLVM.Intrinsics.Declare

Description

Synopsis

data Declare (args :: Ctx CrucibleType) (ret :: CrucibleType) = Declare {
- decName :: Symbol
- decArgs :: Assignment TypeRepr args
- decRet :: TypeRepr ret
}
data SomeDeclare = SomeDeclare (Declare args ret)
fromHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). FnHandle args ret -> Declare args ret
fromSomeHandle :: SomeHandle -> SomeDeclare
fromLLVM :: forall (wptr :: Natural) m. (?lc :: TypeContext, HasPtrWidth wptr, MonadFail m) => Declare -> m SomeDeclare
fromLLVMWithWarnings :: forall (wptr :: Natural) p sym ext rtp (l :: Ctx CrucibleType) (a :: CrucibleType). (?lc :: TypeContext, HasPtrWidth wptr) => [Declare] -> OverrideSim p sym ext rtp l a [SomeDeclare]

Documentation

data Declare (args :: Ctx CrucibleType) (ret :: CrucibleType) Source #

The declaration of a function.

Used primarily for matching LLVM overrides to the declarations in LLVM modules or S-expression programs.

Constructors

Declare
Fields decName :: Symbol decArgs :: Assignment TypeRepr args decRet :: TypeRepr ret

Instances

Instances details

Show (Declare args ret) Source #
Instance details Defined in Lang.Crucible.LLVM.Intrinsics.Declare Methods showsPrec :: Int -> Declare args ret -> ShowS # show :: Declare args ret -> String # showList :: [Declare args ret] -> ShowS #

data SomeDeclare Source #

Constructors

SomeDeclare (Declare args ret)

fromHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). FnHandle args ret -> Declare args ret Source #

fromSomeHandle :: SomeHandle -> SomeDeclare Source #

fromLLVM :: forall (wptr :: Natural) m. (?lc :: TypeContext, HasPtrWidth wptr, MonadFail m) => Declare -> m SomeDeclare Source #

fromLLVMWithWarnings :: forall (wptr :: Natural) p sym ext rtp (l :: Ctx CrucibleType) (a :: CrucibleType). (?lc :: TypeContext, HasPtrWidth wptr) => [Declare] -> OverrideSim p sym ext rtp l a [SomeDeclare] Source #

Apply fromLLVM in a loop, warning on failures