Frama-C API - Engine_Subset
Subset of Engine_sig.S required by this functor.
include Engine_abstractions_sig.S
module Ctx : Engine_abstractions_sig.Contextmodule Val : Engine_abstractions_sig.Value with type context = Ctx.tmodule Loc : Engine_abstractions_sig.Location with type value = Val.tmodule Dom : Engine_abstractions_sig.Domain with type value = Val.t and type location = Loc.location and type context = Ctx.tmodule Eval : Evaluation_sig.S with type state = Dom.t and type context = Ctx.t and type value = Val.t and type loc = Loc.location and type origin = Dom.originmodule Initialization : Engine_sig.Initialization with type state = Dom.tmodule Transfer_stmt : Engine_sig.Transfer_stmt with type state = Dom.tmodule Transfer_logic : Engine_sig.Transfer_logic with type state = Dom.tmodule Transfer_specification : sig ... end