module Generator: sig
.. end
module type S = sig
.. end
module Make: functor (
M
:
sig
val name : string
val default : Cil_types.kernel_function -> bool
val parameter : Typed_parameter.t
val additional_parameters : Typed_parameter.t list
end
) ->
sig
.. end
module Signed: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Mem_access: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : Typed_parameter.t list
end
)
module Div_mod: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Shift: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Downcast: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Unsigned_overflow: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Unsigned_downcast: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Float_to_int: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
module Called_precond: Make
(
sig
val name : string
val default : Kernel_function.t -> bool
val parameter : Typed_parameter.t
val additional_parameters : 'a list
end
)
val proxy : State_builder.Proxy.t
val self : State.t
val precond_status : unit ->
string *
(Called_precond.H.key -> Called_precond.H.data -> unit) *
(Called_precond.H.key -> Called_precond.H.data)
val signed_status : unit ->
string * (Signed.H.key -> Signed.H.data -> unit) *
(Signed.H.key -> Signed.H.data)
val div_mod_status : unit ->
string * (Div_mod.H.key -> Div_mod.H.data -> unit) *
(Div_mod.H.key -> Div_mod.H.data)
val shift_status : unit ->
string * (Shift.H.key -> Shift.H.data -> unit) *
(Shift.H.key -> Shift.H.data)
val downcast_status : unit ->
string * (Downcast.H.key -> Downcast.H.data -> unit) *
(Downcast.H.key -> Downcast.H.data)
val mem_access_status : unit ->
string *
(Mem_access.H.key -> Mem_access.H.data -> unit) *
(Mem_access.H.key -> Mem_access.H.data)
val float_to_int_status : unit ->
string *
(Float_to_int.H.key -> Float_to_int.H.data -> unit) *
(Float_to_int.H.key -> Float_to_int.H.data)
val unsigned_overflow_status : unit ->
string *
(Unsigned_overflow.H.key ->
Unsigned_overflow.H.data -> unit) *
(Unsigned_overflow.H.key -> Unsigned_overflow.H.data)
val unsigned_downcast_status : unit ->
string *
(Unsigned_downcast.H.key ->
Unsigned_downcast.H.data -> unit) *
(Unsigned_downcast.H.key -> Unsigned_downcast.H.data)
val all_status : unit ->
(string *
(Called_precond.H.key -> Called_precond.H.data -> unit) *
(Called_precond.H.key -> Called_precond.H.data))
list
val emitter : Emitter.t