Frama-C API - Engine_Subset
Subset of Engine_sig.S required for 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 Transfer_inout : Engine_sig.Transfer_inout with type location = Loc.location and type value = Val.t and type valuation = Eval.Valuation.tmodule Interferences : Engine_sig.Interferences with type state = Dom.tmodule Compute : Engine_sig.Compute with type state = Dom.t and type value = Val.t and type loc = Loc.locationUsed to interpret function calls.