| Copyright | (c) Galois Inc 2019 |
|---|---|
| License | BSD3 |
| Maintainer | Andrei Stefanescu <andrei@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
Lang.Crucible.Simulator.Cut
Description
This module provides execution features for changing the state on cutpoints.
Synopsis
- cutAndReturn :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType) p rtp. (IsSymInterface sym, IsSyntaxExtension ext) => CFG ext blocks init ret -> CutpointName -> Assignment TypeRepr args -> TypeRepr ret -> OverrideSim p sym ext rtp args ret (RegValue sym ret) -> HashMap SomeHandle [CutpointName] -> IO (ExecutionFeature p sym ext rtp)
Documentation
cutAndReturn :: forall sym ext (blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType) p rtp. (IsSymInterface sym, IsSyntaxExtension ext) => CFG ext blocks init ret -> CutpointName -> Assignment TypeRepr args -> TypeRepr ret -> OverrideSim p sym ext rtp args ret (RegValue sym ret) -> HashMap SomeHandle [CutpointName] -> IO (ExecutionFeature p sym ext rtp) Source #
This execution feature registers an override for a cutpoint. The override summarizes the execution from the cutpoint to the return from the function (similar to a tail call). This feature requires a map from each function handle to the list of cutpoints in the respective function with this execution feature.