functor (KF : sig val kf : Kernel_function.t end) ->
sig
val join2_stmts :
Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t
type path_bound = Integer.t option
val add_path_bounds :
Integer.t option -> Integer.t option -> Integer.t option
type abstract_value =
Slevel_analysis.Specific.path_bound * Cil_types.stmt
val join2 :
Integer.t option * Cil_datatype.Stmt.t ->
Integer.t option * Cil_datatype.Stmt.t ->
Integer.t option * Cil_datatype.Stmt.t
val join :
(Integer.t option * Cil_datatype.Stmt.t) list ->
Integer.t option * Cil_datatype.Stmt.t
val mu :
(Integer.t option * Loop_analysis.Loop_Max_Iteration.key ->
Integer.t option * 'a) ->
Integer.t option * Loop_analysis.Loop_Max_Iteration.key ->
Integer.t option * Loop_analysis.Loop_Max_Iteration.key
val kf : Kernel_function.t
val compile_node :
Cil_datatype.Stmt.t ->
'a * Cil_datatype.Stmt.t ->
(Cil_datatype.Stmt.t Region_analysis.edge * ('a * Cil_datatype.Stmt.t))
list
end