Copyright | (c) Galois Inc 2015 |
---|---|
License | BSD3 |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Lang.Crucible.CFG.ExtractSubgraph
Description
Documentation
extractSubgraph :: (KnownCtx TypeRepr init, KnownRepr TypeRepr ret) => CFG ext blocks init ret -> Set (BlockID blocks (EmptyCtx ::> ret)) -> BlockID blocks init -> HandleAllocator -> IO (Maybe (SomeCFG ext init ret)) Source #
Given a CFG cfg
, a set of blocks cuts
that take the return type as their sole
argument, and a block bi
that takes the CFG's init type as its sole argument,
construct a CFG that is a maximal subgraph starting at bi
and not entering any
block in cuts
. If the original graph would enter a block in cuts
, the value
passed to that block is returned. If bi
, then whenever the subgraph
would transition to member
cutsbi
, it returns the value that would be passed to bi
instead.