| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Instantiation.SymbolicPropagation
Contents
Description
Synopsis
- get_invariant :: FContext -> Int -> Maybe Predicate
- init_pred :: FContext -> String -> Invariants -> Set (NodeInfo, Predicate) -> Set SStatePart -> Predicate
- invariant_to_finit :: FContext -> Predicate -> FInit
- join_finit :: FContext -> FInit -> FInit -> FInit
- gather_stateparts :: Invariants -> Set (NodeInfo, Predicate) -> Set SStatePart
Documentation
get_invariant :: FContext -> Int -> Maybe Predicate Source #
Get the currently known invariant for the given instruction address
Arguments
| :: FContext | The current context |
| -> String | The current function |
| -> Invariants | The currently available invariants |
| -> Set (NodeInfo, Predicate) | The currently known postconditions |
| -> Set SStatePart | The currently known stateparts of the function |
| -> Predicate |
The initial predicate.
invariant_to_finit :: FContext -> Predicate -> FInit Source #
Convert the current invariant into a function initialisation
join_finit :: FContext -> FInit -> FInit -> FInit Source #
The join between two function initialisations
Arguments
| :: Invariants | The currently available invariants |
| -> Set (NodeInfo, Predicate) | The currently known postconditions |
| -> Set SStatePart |
Given the currently known invariants and postconditions, gather all stateparts occurring in the current function.