module Specific: functor (
KF
:
sig
val kf : Kernel_function.t
end
) ->
sig
.. end
Parameters: |
KF |
: |
sig val kf: Kernel_function.t end
|
|
val join2_stmts : Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t
val add_path_bounds : Integer.t option -> Integer.t option -> Integer.t option
type
abstract_value = Slevel_analysis.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