| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
OutputGeneration.Retrieval
Synopsis
- ctxt_get_instructions :: Context -> Set Instruction
- ctxt_get_function_entries :: Context -> Set Int
- ctxt_get_function_summary :: Num a => Context -> Int -> (a, (FInit, Maybe FReturnBehavior))
- ctxt_mk_function_boundary :: Num a => Context -> Int -> (a, [Char])
- ctxt_get_inv :: Context -> Word64 -> (Word64, Maybe [(Word64, Predicate)])
- ctxt_resolve_mem_operands :: Context -> [(Word64, Word64, [Maybe SValue])]
- ctxt_get_instruction :: Context -> Int -> IO Instruction
- ctxt_get_instruction_addresses :: Context -> Set Word64
- ctxt_get_controlflow :: Context -> Word64 -> IO (Word64, [Word64])
Documentation
ctxt_get_instructions :: Context -> Set Instruction Source #
Retrieves a set of instructions.
ctxt_get_function_summary :: Num a => Context -> Int -> (a, (FInit, Maybe FReturnBehavior)) Source #
Retrieves function summaries (preconditions, postconditions)
ctxt_mk_function_boundary :: Num a => Context -> Int -> (a, [Char]) Source #
Retrieves a textual representation of the function boundaries
ctxt_get_inv :: Context -> Word64 -> (Word64, Maybe [(Word64, Predicate)]) Source #
Given an address a, retrieve all invariants (the address may occur in multiple functions).
ctxt_resolve_mem_operands :: Context -> [(Word64, Word64, [Maybe SValue])] Source #
Retrieve an overview of memory operands Returns per instruction a tuple (entry, addr, ptrs). Here: entry is the entry address of the function of the instruction, addr is the address of the instruction ptrs is a list of symbolic pointers for each operand (or Nothing if not a memory-operand)
ctxt_get_instruction :: Context -> Int -> IO Instruction Source #
Retrieve instruction for a given instruction address, both as datastructure and pretty-printed