Frama-C API - `S`

The four abstractions: values, locations, states and evaluation context, plus the evaluation engine for these abstractions.

include Engine_abstractions_sig.S

module Ctx : Engine_abstractions_sig.Context

module Val : Engine_abstractions_sig.Value with type context = Ctx.t

module Loc : Engine_abstractions_sig.Location with type value = Val.t

module Dom : Engine_abstractions_sig.Domain with type value = Val.t and type location = Loc.location and type context = Ctx.t

module 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.origin

module Transfer_inout : Transfer_inout with type location = Loc.location and type value = Val.t and type valuation = Eval.Valuation.t

module Transfer_stmt : Transfer_stmt with type state = Dom.t

module Transfer_logic : Transfer_logic with type state = Dom.t

module Transfer_specification : Transfer_specification with type state = Dom.t and type value = Val.t and type location = Loc.location

module Initialization : Initialization with type state = Dom.t

module Iterator : Iterator with type state = Dom.t

module Compute : Compute with type state = Dom.t and type value = Val.t and type loc = Loc.location

module Interferences : Interferences with type state = Dom.t

Frama-C API - S

Frama-C API - `S`