foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
Safe HaskellSafe-Inferred
LanguageHaskell2010

WithAbstractSymbolicValues.InstanceOfAbstractPredicates

Orphan instances

(Show v, Ord v, BinaryClass bin, WithAbstractSymbolicValues (bin, Config, L0 (Sstate v p) (FInit v p) v, Word64) v p) => WithAbstractPredicates bin (Sstate v p) (FInit v p) v Source # 
Instance details

Methods

symbolically_execute :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Bool -> [Instruction] -> Maybe [Instruction] -> State (Sstate v p, VCS v) () Source #

verify_postcondition :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Bool Source #

finit_to_init_pred :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> Sstate v p Source #

pred_to_finit :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> FInit v p Source #

resolve_indirection :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> [Instruction] -> Indirections Source #

is_weaker_than :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Bool Source #

join_preds :: LiftingEntry bin (Sstate v p) (FInit v p) v -> Sstate v p -> Sstate v p -> Sstate v p Source #

join_finits :: LiftingEntry bin (Sstate v p) (FInit v p) v -> FInit v p -> FInit v p -> FInit v p Source #

new_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p Source #

pp_finit :: Lifting bin (Sstate v p) (FInit v p) v -> FInit v p -> String Source #