foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.VerificationCondition

Documentation

data PointerAnalysisResult v Source #

Constructors

PointerAnalysisResult 

Fields

Instances

Instances details
Generic (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Associated Types

type Rep (PointerAnalysisResult v) :: Type -> Type #

Methods

from :: PointerAnalysisResult v -> Rep (PointerAnalysisResult v) x #

to :: Rep (PointerAnalysisResult v) x -> PointerAnalysisResult v #

Show v => Show (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

showsPrec :: Int -> PointerAnalysisResult v -> ShowS #

show :: PointerAnalysisResult v -> String #

showList :: [PointerAnalysisResult v] -> ShowS #

Serialize v => Serialize (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

put :: Putter (PointerAnalysisResult v) #

get :: Get (PointerAnalysisResult v) #

NFData v => NFData (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

rnf :: PointerAnalysisResult v -> () #

Eq v => Eq (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

(==) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

(/=) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

Ord v => Ord (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

compare :: PointerAnalysisResult v -> PointerAnalysisResult v -> Ordering #

(<) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

(<=) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

(>) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

(>=) :: PointerAnalysisResult v -> PointerAnalysisResult v -> Bool #

max :: PointerAnalysisResult v -> PointerAnalysisResult v -> PointerAnalysisResult v #

min :: PointerAnalysisResult v -> PointerAnalysisResult v -> PointerAnalysisResult v #

type Rep (PointerAnalysisResult v) Source # 
Instance details

Defined in Data.VerificationCondition

type Rep (PointerAnalysisResult v) = D1 ('MetaData "PointerAnalysisResult" "Data.VerificationCondition" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "PointerAnalysisResult" 'PrefixI 'True) (S1 ('MetaSel ('Just "pa_mem_write") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe v)) :*: S1 ('MetaSel ('Just "pa_mem_reads") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Maybe v])))

show_pars :: Show a => [Maybe a] -> [Char] Source #

data VerificationCondition v Source #

Constructors

FunctionPointers Word64 IntSet

A set of function pointers passed to a function

PointerAnalysis Word64 (PointerAnalysisResult v)

A pointer analysis result for the instruction at the address

Instances

Instances details
Generic (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Associated Types

type Rep (VerificationCondition v) :: Type -> Type #

Methods

from :: VerificationCondition v -> Rep (VerificationCondition v) x #

to :: Rep (VerificationCondition v) x -> VerificationCondition v #

Show v => Show (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

showsPrec :: Int -> VerificationCondition v -> ShowS #

show :: VerificationCondition v -> String #

showList :: [VerificationCondition v] -> ShowS #

Serialize v => Serialize (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

put :: Putter (VerificationCondition v) #

get :: Get (VerificationCondition v) #

NFData v => NFData (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

rnf :: VerificationCondition v -> () #

Eq v => Eq (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

(==) :: VerificationCondition v -> VerificationCondition v -> Bool #

(/=) :: VerificationCondition v -> VerificationCondition v -> Bool #

Ord v => Ord (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

Methods

compare :: VerificationCondition v -> VerificationCondition v -> Ordering #

(<) :: VerificationCondition v -> VerificationCondition v -> Bool #

(<=) :: VerificationCondition v -> VerificationCondition v -> Bool #

(>) :: VerificationCondition v -> VerificationCondition v -> Bool #

(>=) :: VerificationCondition v -> VerificationCondition v -> Bool #

max :: VerificationCondition v -> VerificationCondition v -> VerificationCondition v #

min :: VerificationCondition v -> VerificationCondition v -> VerificationCondition v #

type Rep (VerificationCondition v) Source # 
Instance details

Defined in Data.VerificationCondition

type Rep (VerificationCondition v) = D1 ('MetaData "VerificationCondition" "Data.VerificationCondition" "foxdec-0.1.0.0-DGuc5MMkhbvOBLAebyTd5" 'False) (C1 ('MetaCons "FunctionPointers" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IntSet)) :+: C1 ('MetaCons "PointerAnalysis" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (PointerAnalysisResult v))))

type VCS v = Set (VerificationCondition v) Source #

gather_pa_results :: VCS v -> IntMap (PointerAnalysisResult v) Source #