| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
WithAbstractPredicates.GenerateInvariants
Synopsis
- generate_invariants :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> finit -> (IntMap pred, VCS v)
- invs_to_PA :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IntMap pred -> IntMap (PointerAnalysisResult v)
- invs_to_post :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IntMap pred -> Postcondition pred
- withEntry :: d -> (a, b, c) -> (a, b, c, d)
- withoutEntry :: (a, b, c, d) -> (a, b, c)
- get_postcondition_for_block :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> Int -> [Instruction] -> IntMap pred -> (pred, VCS v)
- propagate :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> State (IntMap pred, Set (Int, Int), VCS v) ()
- out_edges :: CFG -> Int -> Set (Int, Key)
Documentation
generate_invariants :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> finit -> (IntMap pred, VCS v) Source #
Start propagation at the given entry address with the given initial predicate. Returns a set of invariants, i.e., a mapping of instruction addresses to predicates.
Assumes blockID 0 is start of function
invs_to_PA :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IntMap pred -> IntMap (PointerAnalysisResult v) Source #
invs_to_post :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> CFG -> IntMap pred -> Postcondition pred Source #
withoutEntry :: (a, b, c, d) -> (a, b, c) Source #
get_postcondition_for_block :: WithAbstractPredicates bin pred finit v => LiftingEntry bin pred finit v -> Int -> [Instruction] -> IntMap pred -> (pred, VCS v) Source #