foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellNone
LanguageHaskell2010

Analysis.Context

Description

The context stores, among others, information obtained during verification, such as CFGs, invariants, etc. (see Context). Module VerificationReportInterface provides functions for obtaining and interfacing with a Context.

Synopsis

Documentation

data FContext Source #

The context augmented with information on the current function

Constructors

FContext 

Fields

Instances

Instances details
Propagator FContext Predicate Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

SymbolicExecutable FContext SValue SPointer Source # 
Instance details

Defined in Instantiation.SymbolicPropagation

Methods

sseparate :: FContext -> String -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

senclosed :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

salias :: FContext -> SPointer -> RegionSize -> SPointer -> RegionSize -> Bool Source #

ssensitive :: FContext -> SPointer -> RegionSize -> SValue -> Bool Source #

sread_from_ro_data :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

smk_mem_addresses :: FContext -> String -> SValue -> Set SPointer Source #

sjoin_values :: Foldable t => FContext -> String -> t SValue -> SValue Source #

swiden_values :: FContext -> String -> SValue -> SValue Source #

sjoin_pointers :: FContext -> [SPointer] -> [SPointer] Source #

top :: FContext -> String -> SValue Source #

ssemantics :: FContext -> String -> SymbolicOperation SValue -> SValue Source #

sflg_semantics :: FContext -> SValue -> Instruction -> FlagStatus -> FlagStatus Source #

simmediate :: Integral i => FContext -> i -> SValue Source #

smk_init_reg_value :: FContext -> Register -> SValue Source #

smk_init_mem_value :: FContext -> String -> SPointer -> RegionSize -> SValue Source #

scall :: FContext -> Bool -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

sjump :: FContext -> Instruction -> State (Sstate SValue SPointer, VCS) () Source #

stry_jump_targets :: FContext -> SValue -> Maybe (Set ResolvedJumpTarget) Source #

stry_immediate :: FContext -> SValue -> Maybe Word64 Source #

stry_deterministic :: FContext -> SValue -> Maybe SimpleExpr Source #

stry_relocation :: FContext -> SPointer -> RegionSize -> Maybe SValue Source #

saddress_has_instruction :: FContext -> Word64 -> Bool Source #

read_binary :: String -> String -> IO (Maybe Binary) Source #

Reading a binary given a filename (ELF or MachO)

data CFG Source #

A control flow graph with blocks and edges. A blockID (represented as an Int) is a unique identifier of a basic block. We store basic blocks twice: once as addresses, and once as instructions.

Constructors

CFG 

Fields

Instances

Instances details
Eq CFG Source # 
Instance details

Defined in Analysis.Context

Methods

(==) :: CFG -> CFG -> Bool #

(/=) :: CFG -> CFG -> Bool #

Show CFG Source # 
Instance details

Defined in Analysis.Context

Methods

showsPrec :: Int -> CFG -> ShowS #

show :: CFG -> String #

showList :: [CFG] -> ShowS #

Generic CFG Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep CFG :: Type -> Type #

Methods

from :: CFG -> Rep CFG x #

to :: Rep CFG x -> CFG #

Serialize CFG Source # 
Instance details

Defined in Analysis.Context

Methods

put :: Putter CFG #

get :: Get CFG #

NFData CFG Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: CFG -> () #

type Rep CFG Source # 
Instance details

Defined in Analysis.Context

data JumpTable Source #

A jump table with : index: an operand containing a bounded index at the beginning of execution of the block bound: the bound on idx trgt: the operand containg the jump target at the end of execution of the block tbl: a table from values of idx to resulting jump targets

Instances

Instances details
Eq JumpTable Source # 
Instance details

Defined in Analysis.Context

Show JumpTable Source # 
Instance details

Defined in Analysis.Context

Generic JumpTable Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep JumpTable :: Type -> Type #

Serialize JumpTable Source # 
Instance details

Defined in Analysis.Context

NFData JumpTable Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: JumpTable -> () #

type Rep JumpTable Source # 
Instance details

Defined in Analysis.Context

type Rep JumpTable = D1 ('MetaData "JumpTable" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "JumpTable" 'PrefixI 'True) ((S1 ('MetaSel ('Just "jtbl_index") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Operand) :*: S1 ('MetaSel ('Just "jtbl_bound") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "jtbl_target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Operand) :*: S1 ('MetaSel ('Just "jtbl_table") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (IntMap Word64)))))

data Indirection Source #

An indirection is either a jump table or a set of resolved jump targets

Instances

Instances details
Eq Indirection Source # 
Instance details

Defined in Analysis.Context

Show Indirection Source # 
Instance details

Defined in Analysis.Context

Generic Indirection Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep Indirection :: Type -> Type #

Serialize Indirection Source # 
Instance details

Defined in Analysis.Context

NFData Indirection Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: Indirection -> () #

type Rep Indirection Source # 
Instance details

Defined in Analysis.Context

type Rep Indirection = D1 ('MetaData "Indirection" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Indirection_JumpTable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 JumpTable)) :+: (C1 ('MetaCons "Indirection_Resolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Set ResolvedJumpTarget))) :+: C1 ('MetaCons "Indirection_Unresolved" 'PrefixI 'False) (U1 :: Type -> Type)))

type Indirections = IntMap Indirection Source #

Per instruction address, a set of possibly resolved jump targets

data VerificationResult Source #

An enumeration indicating the result of verification over a function

Constructors

VerificationSuccess

Function was succesfully verified

VerificationSuccesWithAssumptions

Function was succesfully verified, but required assertions

VerificationUnresolvedIndirection

Function contains an unresolved indirection

VerificationError String

There was some verification error, e.g., return adresss overwrite

Unverified

The function has not been verified.

Instances

Instances details
Eq VerificationResult Source # 
Instance details

Defined in Analysis.Context

Show VerificationResult Source # 
Instance details

Defined in Analysis.Context

Generic VerificationResult Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep VerificationResult :: Type -> Type #

Serialize VerificationResult Source # 
Instance details

Defined in Analysis.Context

NFData VerificationResult Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: VerificationResult -> () #

type Rep VerificationResult Source # 
Instance details

Defined in Analysis.Context

type Rep VerificationResult = D1 ('MetaData "VerificationResult" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) ((C1 ('MetaCons "VerificationSuccess" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VerificationSuccesWithAssumptions" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VerificationUnresolvedIndirection" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "VerificationError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 String)) :+: C1 ('MetaCons "Unverified" 'PrefixI 'False) (U1 :: Type -> Type))))

type Predicate = Sstate SValue SPointer Source #

Predicates: symbolic states

type Invariants = IntMap Predicate Source #

Invariants: a mapping of blockIDs to predicates

data NodeInfo Source #

For each leaf-node in a CFG we store the following info. (TODO MOVE?)

Constructors

Normal

The basic block behaves normally, e.g., a ret

UnresolvedIndirection

The basic block ends in an unresolved indirection

Terminal

The basic blocks ends with, e.g., a call to exit()

Instances

Instances details
Eq NodeInfo Source # 
Instance details

Defined in Analysis.Context

Ord NodeInfo Source # 
Instance details

Defined in Analysis.Context

Show NodeInfo Source # 
Instance details

Defined in Analysis.Context

Generic NodeInfo Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep NodeInfo :: Type -> Type #

Methods

from :: NodeInfo -> Rep NodeInfo x #

to :: Rep NodeInfo x -> NodeInfo #

Serialize NodeInfo Source # 
Instance details

Defined in Analysis.Context

NFData NodeInfo Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: NodeInfo -> () #

type Rep NodeInfo Source # 
Instance details

Defined in Analysis.Context

type Rep NodeInfo = D1 ('MetaData "NodeInfo" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Normal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnresolvedIndirection" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Terminal" 'PrefixI 'False) (U1 :: Type -> Type)))

type Postconditions = Set (NodeInfo, Predicate) Source #

Postconditions: for each final block the NodeInfo and the final predicate after execution of the block

data PointerDomain Source #

An abstract domain for pointers

Instances

Instances details
Eq PointerDomain Source # 
Instance details

Defined in Analysis.Context

Ord PointerDomain Source # 
Instance details

Defined in Analysis.Context

Show PointerDomain Source # 
Instance details

Defined in Analysis.Context

Generic PointerDomain Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep PointerDomain :: Type -> Type #

ToJSON PointerDomain Source # 
Instance details

Defined in OutputGeneration.JSON

Serialize PointerDomain Source # 
Instance details

Defined in Analysis.Context

NFData PointerDomain Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: PointerDomain -> () #

type Rep PointerDomain Source # 
Instance details

Defined in Analysis.Context

type Rep PointerDomain = D1 ('MetaData "PointerDomain" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Domain_Bases" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (NESet PointerBase))) :+: C1 ('MetaCons "Domain_Sources" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (NESet BotSrc))))

data MemRelation Source #

A function initialisation consists of a mapping of registers to symbolic pointers TODO

Constructors

Separate 
Aliassing 
Unknown 

Instances

Instances details
Eq MemRelation Source # 
Instance details

Defined in Analysis.Context

Ord MemRelation Source # 
Instance details

Defined in Analysis.Context

Show MemRelation Source # 
Instance details

Defined in Analysis.Context

Generic MemRelation Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep MemRelation :: Type -> Type #

Serialize MemRelation Source # 
Instance details

Defined in Analysis.Context

NFData MemRelation Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: MemRelation -> () #

type Rep MemRelation Source # 
Instance details

Defined in Analysis.Context

type Rep MemRelation = D1 ('MetaData "MemRelation" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Separate" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Aliassing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type)))

data FInit Source #

Instances

Instances details
Eq FInit Source # 
Instance details

Defined in Analysis.Context

Methods

(==) :: FInit -> FInit -> Bool #

(/=) :: FInit -> FInit -> Bool #

Ord FInit Source # 
Instance details

Defined in Analysis.Context

Methods

compare :: FInit -> FInit -> Ordering #

(<) :: FInit -> FInit -> Bool #

(<=) :: FInit -> FInit -> Bool #

(>) :: FInit -> FInit -> Bool #

(>=) :: FInit -> FInit -> Bool #

max :: FInit -> FInit -> FInit #

min :: FInit -> FInit -> FInit #

Show FInit Source #

Show function initialisation

Instance details

Defined in Analysis.Context

Methods

showsPrec :: Int -> FInit -> ShowS #

show :: FInit -> String #

showList :: [FInit] -> ShowS #

Generic FInit Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep FInit :: Type -> Type #

Methods

from :: FInit -> Rep FInit x #

to :: Rep FInit x -> FInit #

Serialize FInit Source # 
Instance details

Defined in Analysis.Context

Methods

put :: Putter FInit #

get :: Get FInit #

NFData FInit Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: FInit -> () #

type Rep FInit Source # 
Instance details

Defined in Analysis.Context

data FReturnBehavior Source #

A function call

Constructors

Terminating

The function does never return

ReturningWith Predicate

The function returns withg the symbolic changes stored in the predicate

UnknownRetBehavior

It is unknown whether the function returns or not

Instances

Instances details
Eq FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

Ord FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

Show FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

Generic FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep FReturnBehavior :: Type -> Type #

Serialize FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

NFData FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: FReturnBehavior -> () #

type Rep FReturnBehavior Source # 
Instance details

Defined in Analysis.Context

type Rep FReturnBehavior = D1 ('MetaData "FReturnBehavior" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Terminating" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ReturningWith" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Predicate)) :+: C1 ('MetaCons "UnknownRetBehavior" 'PrefixI 'False) (U1 :: Type -> Type)))

data SStatePart Source #

A symbolic state part

Constructors

SSP_Reg Register

A register

SSP_Mem SPointer Int 

Instances

Instances details
Eq SStatePart Source # 
Instance details

Defined in Analysis.Context

Ord SStatePart Source # 
Instance details

Defined in Analysis.Context

Show SStatePart Source # 
Instance details

Defined in Analysis.Context

Generic SStatePart Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep SStatePart :: Type -> Type #

Serialize SStatePart Source # 
Instance details

Defined in Analysis.Context

NFData SStatePart Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: SStatePart -> () #

type Rep SStatePart Source # 
Instance details

Defined in Analysis.Context

data Context_ Source #

The context datastructure.

S: Information Statically obtained by reading from the binary

D: Information Dynamically updated during verification

Constructors

Context_ 

Fields

Instances

Instances details
Generic Context_ Source # 
Instance details

Defined in Analysis.Context

Associated Types

type Rep Context_ :: Type -> Type #

Methods

from :: Context_ -> Rep Context_ x #

to :: Rep Context_ x -> Context_ #

Serialize Context_ Source # 
Instance details

Defined in Analysis.Context

NFData Context_ Source # 
Instance details

Defined in Analysis.Context

Methods

rnf :: Context_ -> () #

type Rep Context_ Source # 
Instance details

Defined in Analysis.Context

type Rep Context_ = D1 ('MetaData "Context_" "Analysis.Context" "foxdec-0.1.0.0-F8J4QQ8bsQELJyhc4kJb0m" 'False) (C1 ('MetaCons "Context_" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "ctxt__config") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Config) :*: S1 ('MetaSel ('Just "ctxt__verbose") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "ctxt__syms") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymbolTable) :*: (S1 ('MetaSel ('Just "ctxt__sections") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SectionsInfo) :*: S1 ('MetaSel ('Just "ctxt__relocs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Set Relocation))))) :*: ((S1 ('MetaSel ('Just "ctxt__dirname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Just "ctxt__name") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)) :*: (S1 ('MetaSel ('Just "ctxt__start") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Just "ctxt__entries") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Graph) :*: S1 ('MetaSel ('Just "ctxt__cfgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap CFG)))))) :*: (((S1 ('MetaSel ('Just "ctxt__calls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap FReturnBehavior)) :*: S1 ('MetaSel ('Just "ctxt__invs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap Invariants))) :*: (S1 ('MetaSel ('Just "ctxt__posts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap Postconditions)) :*: (S1 ('MetaSel ('Just "ctxt__stateparts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap (Set SStatePart))) :*: S1 ('MetaSel ('Just "ctxt__inds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Indirections)))) :*: ((S1 ('MetaSel ('Just "ctxt__finits") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap FInit)) :*: S1 ('MetaSel ('Just "ctxt__vcs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap VCS))) :*: (S1 ('MetaSel ('Just "ctxt__results") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap VerificationResult)) :*: (S1 ('MetaSel ('Just "ctxt__recursions") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (IntMap IntSet)) :*: S1 ('MetaSel ('Just "ctxt__runningtime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int64)))))))

init_finit :: FInit Source #

intialize an empty context based on the command-line parameters

purge_context :: Context -> Context_ Source #

purge the context before exporting it (may save a lot of disk space)

ctxt_symbol_table :: Context -> IntMap Symbol Source #

Getting the symbol table

read_from_ro_datasection Source #

Arguments

:: Context

The context

-> Word64

An address

-> Int

Size, i.e., the number of bytes to read

-> Maybe Word64 

Reading from a read-only data section.

Reads maximally up to 8 bytes. Returns Nothing if the given address is out-of-range.

read_from_datasection Source #

Arguments

:: Context

The context

-> Word64

An address

-> Int

Size, i.e., the number of bytes to read

-> Maybe Word64 

Reading from a writable data section.

Reads maximally up to 8 bytes. Returns Nothing if the given address is out-of-range.

is_roughly_an_address Source #

Arguments

:: Context

The context

-> Word64

An address

-> Bool 

Is the immediate roughly in range to be an address?

find_section_for_address Source #

Arguments

:: Context

The context

-> Word64

An address

-> Maybe (String, String, Word64, Word64) 

Find a section for an address (see SectionsInfo)

find_section_ending_at Source #

Arguments

:: Context

The context

-> Word64

An address

-> Maybe (String, String, Word64, Word64) 

Find a section ending at address (see SectionsInfo)

fetch_instruction Source #

Arguments

:: Context

The context

-> Word64

An address

-> IO (Maybe Instruction) 

Fetching an instruction

Returns Nothing if the given address is out-of-range.

pp_instruction Source #

Arguments

:: Context

The context

-> Instruction

An instruction

-> String 

Pretty printing an instruction

is_assertion :: VerificationCondition -> Bool Source #

Is the given verification condition an assertion?

is_precondition :: VerificationCondition -> Bool Source #

Is the given verification condition a precondition?

is_func_constraint :: VerificationCondition -> Bool Source #

Is the given verification condition a function constraint?

is_functionpointers :: VerificationCondition -> Bool Source #

Is the given verification condition a function pointer introduction?

count_instructions_with_assertions :: Set VerificationCondition -> Int Source #

Count the number of assertions in the set of verification conditions.

ctxt_read_L0 Source #

Arguments

:: String

The directory name

-> String

The file name of the binary

-> IO Context 

Read in the .L0 file from a file with the given file name. May produce an error if no L0 can be read from the file. Returns the L0 stored in the .L0 file.

address_has_instruction :: Integral a => Context -> a -> Bool Source #

Returns true iff an instruction can be fetched from the address.

Orphan instances

Show VerificationCondition Source # 
Instance details

Serialize ResolvedJumpTarget Source # 
Instance details

Serialize Relocation Source # 
Instance details

Serialize SymbolTable Source # 
Instance details

Serialize Symbol Source # 
Instance details

Serialize SectionsInfo Source # 
Instance details

Serialize VerificationCondition Source # 
Instance details

NFData ResolvedJumpTarget Source # 
Instance details

Methods

rnf :: ResolvedJumpTarget -> () #

NFData Relocation Source # 
Instance details

Methods

rnf :: Relocation -> () #

NFData SymbolTable Source # 
Instance details

Methods

rnf :: SymbolTable -> () #

NFData Symbol Source # 
Instance details

Methods

rnf :: Symbol -> () #

NFData SectionsInfo Source # 
Instance details

Methods

rnf :: SectionsInfo -> () #

NFData VerificationCondition Source # 
Instance details

Methods

rnf :: VerificationCondition -> () #