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

WithAbstractSymbolicValues.FInit

Synopsis

Documentation

finit_to_init_sstate :: WithAbstractSymbolicValues ctxt v p => ctxt -> FInit v p -> Sstate v p Source #

The initial predicate.

sstate_to_finit :: WithAbstractSymbolicValues ctxt v p => ctxt -> Sstate v p -> FInit v p Source #

Convert the current invariant into a function initialisation

join_finit :: WithAbstractSymbolicValues ctxt v p => ctxt -> FInit v p -> FInit v p -> FInit v p Source #

The join between two function initialisations

pp_finitC :: (Show p, Show v, Ord p) => FInit v p -> String Source #

Orphan instances

Show p => Show (SStatePart p) Source # 
Instance details

Methods

showsPrec :: Int -> SStatePart p -> ShowS #

show :: SStatePart p -> String #

showList :: [SStatePart p] -> ShowS #

(Eq v, Show v, Show p) => Show (FInit v p) Source #

Show function initialisation

Instance details

Methods

showsPrec :: Int -> FInit v p -> ShowS #

show :: FInit v p -> String #

showList :: [FInit v p] -> ShowS #