sig
module Flags :
sig
type t = {
remove_trivial : bool;
initialized : bool;
mem_access : bool;
div_mod : bool;
shift : bool;
left_shift_negative : bool;
right_shift_negative : bool;
signed_overflow : bool;
unsigned_overflow : bool;
signed_downcast : bool;
unsigned_downcast : bool;
pointer_downcast : bool;
float_to_int : bool;
finite_float : bool;
pointer_call : bool;
pointer_value : bool;
bool_value : bool;
}
val default :
?remove_trivial:bool ->
?initialized:bool ->
?mem_access:bool ->
?div_mod:bool ->
?shift:bool ->
?left_shift_negative:bool ->
?right_shift_negative:bool ->
?signed_overflow:bool ->
?unsigned_overflow:bool ->
?signed_downcast:bool ->
?unsigned_downcast:bool ->
?pointer_downcast:bool ->
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
?pointer_value:bool -> ?bool_value:bool -> unit -> t
val all : t
val none : t
end
module Generator :
sig
module type S =
sig
val is_computed : Kernel_function.t -> bool
val set : Kernel_function.t -> bool -> unit
val accessor : Db.RteGen.status_accessor
end
module Initialized : S
module Mem_access : S
module Pointer_value : S
module Pointer_call : S
module Div_mod : S
module Shift : S
module Left_shift_negative : S
module Right_shift_negative : S
module Signed_overflow : S
module Signed_downcast : S
module Unsigned_overflow : S
module Unsigned_downcast : S
module Pointer_downcast : S
module Float_to_int : S
module Finite_float : S
module Bool_value : S
val all_statuses : Db.RteGen.status_accessor list
val emitter : Emitter.t
val get_registered_annotations :
Cil_types.stmt -> Cil_types.code_annotation list
end
module Visit :
sig
val annotate :
?flags:RteGen.Flags.t -> Cil_types.kernel_function -> unit
val get_annotations_kf :
?flags:RteGen.Flags.t ->
Cil_types.kernel_function -> Cil_types.code_annotation list
val get_annotations_stmt :
?flags:RteGen.Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation list
val get_annotations_exp :
?flags:RteGen.Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list
val get_annotations_lval :
?flags:RteGen.Flags.t ->
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.lval -> Cil_types.code_annotation list
type on_alarm =
Cil_types.kernel_function ->
Cil_types.stmt -> invalid:bool -> Alarms.alarm -> unit
type 'a iterator =
?flags:RteGen.Flags.t ->
RteGen.Visit.on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
val iter_lval : Cil_types.lval RteGen.Visit.iterator
val iter_exp : Cil_types.exp RteGen.Visit.iterator
val iter_instr : Cil_types.instr RteGen.Visit.iterator
val iter_stmt : Cil_types.stmt RteGen.Visit.iterator
val register :
Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
invalid:bool -> Alarms.alarm -> Cil_types.code_annotation * bool
end
end