| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Analysis.SymbolicExecution
Contents
Description
Synopsis
- tau_block :: FContext -> [Instruction] -> Maybe [Instruction] -> Pred -> (Pred, VCS)
- init_pred :: FContext -> Invariants -> Set (NodeInfo, Pred) -> Set StatePart -> Pred
- gather_stateparts :: Invariants -> Set (NodeInfo, Pred) -> Set StatePart
- invariant_to_finit :: FContext -> Pred -> FInit
- join_finit :: FContext -> FInit -> FInit -> FInit
- get_invariant :: FContext -> Int -> Maybe Pred
Documentation
Arguments
| :: FContext | The context |
| -> [Instruction] | The instructions of the basic block |
| -> Maybe [Instruction] | Optionally, the instructions of the next block if symbolically executing an edge in a CFG. |
| -> Pred | The predicate to be transformed |
| -> (Pred, VCS) |
Do predicate transformation over a basic block in a CFG.
Given an edge in the CFG from none block to another, perform predicate transformation.
Parameter insts' is needed to set the flags properly. If Nothing is supplied, the flags are overapproximatively set to None
Arguments
| :: FContext | The current context |
| -> Invariants | The currently available invariants |
| -> Set (NodeInfo, Pred) | The currently known postconditions |
| -> Set StatePart | The currently known stateparts of the function |
| -> Pred |
The initial predicate.
Arguments
| :: Invariants | The currently available invariants |
| -> Set (NodeInfo, Pred) | The currently known postconditions |
| -> Set StatePart |
Given the currently known invariants and postconditions, gather all stateparts occurring in the current function.
invariant_to_finit :: FContext -> Pred -> FInit Source #
Convert the current invariant into a function initialisation
join_finit :: FContext -> FInit -> FInit -> FInit Source #
The join between two function initialisations
get_invariant :: FContext -> Int -> Maybe Pred Source #
Get the invariant for a given instruction address for a given function entry