Module `LowerHil.Make`

Functor for turning HIL transfer functions into SIL transfer functions

Parameters

TransferFunctions : TransferFunctions.HIL
HilConfig : HilConfig

Signature

module CFG : ProcCfg.S with type t = TransferFunctions.CFG.t and type instrs_dir = TransferFunctions.CFG.instrs_dir and type Node.t = TransferFunctions.CFG.Node.t and type Node.id = TransferFunctions.CFG.Node.id and module Node.IdMap = TransferFunctions.CFG.Node.IdMap and module Node.IdSet = TransferFunctions.CFG.Node.IdSet

module Domain : module type of sig ... end

type analysis_data = TransferFunctions.analysis_data

val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> ProcCfg.InstrNode.instr_index -> IR.Sil.instr -> Domain.t
val pp_session_name : CFG.Node.t -> Stdlib.Format.formatter -> unit