| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
WithAbstractPredicates.Class
Documentation
class (Show v, Ord v, Eq pred, Eq finit, BinaryClass bin, Show pred, Show finit) => WithAbstractPredicates bin pred finit v | pred -> finit, pred -> v where Source #
Methods
symbolically_execute :: LiftingEntry bin pred finit v -> Bool -> [Instruction] -> Maybe [Instruction] -> State (pred, VCS v) () Source #
verify_postcondition :: LiftingEntry bin pred finit v -> pred -> Bool Source #
finit_to_init_pred :: LiftingEntry bin pred finit v -> finit -> pred Source #
pred_to_finit :: LiftingEntry bin pred finit v -> pred -> finit Source #
resolve_indirection :: LiftingEntry bin pred finit v -> pred -> [Instruction] -> Indirections Source #
is_weaker_than :: LiftingEntry bin pred finit v -> pred -> pred -> Bool Source #
join_preds :: LiftingEntry bin pred finit v -> pred -> pred -> pred Source #
join_finits :: LiftingEntry bin pred finit v -> finit -> finit -> finit Source #
new_finit :: Lifting bin pred finit v -> finit Source #
pp_finit :: Lifting bin pred finit v -> finit -> String Source #