sig
type syntactic_context =
SyNone
| SyCallResult
| SyBinOp of Cil_types.exp * Cil_types.binop * Cil_types.exp *
Cil_types.exp
| SyUnOp of Cil_types.exp
| SyMem of Cil_types.lval
| SyMemLogic of Cil_types.term
| SySep of Cil_types.lval * Cil_types.lval
val start_stmt : Cil_types.kinstr -> unit
val end_stmt : unit -> unit
val current_stmt : unit -> Cil_types.kinstr
val set_syntactic_context : CilE.syntactic_context -> unit
val get_syntactic_context :
unit -> Cil_types.kinstr * CilE.syntactic_context
type alarm_behavior = {
a_log : (Emitter.t * (Format.formatter -> unit)) option;
a_call : unit -> unit;
}
val do_warn :
CilE.alarm_behavior ->
(Emitter.t * (Format.formatter -> unit) -> unit) -> unit
val a_ignore : CilE.alarm_behavior
type warn_mode = {
imprecision_tracing : CilE.alarm_behavior;
defined_logic : CilE.alarm_behavior;
unspecified : CilE.alarm_behavior;
others : CilE.alarm_behavior;
}
val warn_all_mode :
Emitter.t -> (Format.formatter -> unit) -> CilE.warn_mode
val warn_none_mode : CilE.warn_mode
val warn_div : CilE.warn_mode -> unit
val warn_shift : CilE.warn_mode -> int -> unit
val warn_shift_left_positive : CilE.warn_mode -> unit
val warn_mem_read : CilE.warn_mode -> unit
val warn_mem_write : CilE.warn_mode -> unit
val warn_integer_overflow :
CilE.warn_mode ->
signed:bool -> min:Integer.t option -> max:Integer.t option -> unit
val warn_float_to_int_overflow :
CilE.warn_mode ->
Integer.t option ->
Integer.t option -> (Format.formatter -> unit) -> unit
val warn_index : CilE.warn_mode -> positive:bool -> range:string -> unit
val warn_pointer_comparison : CilE.warn_mode -> unit
val warn_valid_string : CilE.warn_mode -> unit
val warn_pointer_subtraction : CilE.warn_mode -> unit
val warn_nan_infinite :
CilE.warn_mode ->
Cil_types.fkind option -> (Format.formatter -> unit) -> unit
val warn_uninitialized : CilE.warn_mode -> unit
val warn_escapingaddr : CilE.warn_mode -> unit
val warn_separated : CilE.warn_mode -> unit
val warn_overlap :
Locations.location * Locations.location -> CilE.warn_mode -> unit
end