crux-llvm-0.11.0.0: A verification tool for C programs.
Safe HaskellNone
LanguageHaskell2010

Crux.LLVM.Overrides

Synopsis

Documentation

cruxLLVMOverrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) personality ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => Proxy# arch -> [OverrideTemplate (personality sym) sym ext arch] Source #

svCompOverrides :: forall sym (wptr :: Natural) personality ext (arch :: LLVMArch). (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => [OverrideTemplate (personality sym) sym ext arch] Source #

cbmcOverrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) personality ext. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions) => Proxy# arch -> [OverrideTemplate (personality sym) sym ext arch] Source #

type ArchOk (arch :: LLVMArch) = HasPtrWidth (ArchWidth arch) Source #

This happens quite a lot, so just a shorter name

type TPtr (arch :: LLVMArch) = LLVMPointerType (ArchWidth arch) Source #