Frama_c_kernel_base.Cil_state_builderFunctors for building computations which use kernel datatypes.
module Stmt_set_ref
(_ : Fclib.State_builder.Info) :
Fclib.State_builder.Set_ref with type elt = Cil_types.stmtmodule Kinstr_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.kinstr
and type data = Data.tmodule Stmt_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.stmt
and type data = Data.tmodule Varinfo_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.varinfo
and type data = Data.tmodule Exp_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.exp
and type data = Data.tmodule Lval_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.lval
and type data = Data.tmodule Kernel_function_hashtbl
(Data : Fclib.Datatype.S)
(_ : Fclib.State_builder.Info_with_size) :
Fclib.State_builder.Hashtbl
with type key = Cil_types.kernel_function
and type data = Data.t