Module Value_util

module Value_util: sig .. end
Callstacks related types and functions

A call_stack is a list, telling which function was called at which site. The head of the list tells about the latest call.



Callstacks related types and functions
type call_site = Cil_types.kernel_function * Cil_types.kinstr 
A call_stack is a list, telling which function was called at which site. The head of the list tells about the latest call.
type callstack = call_site list 
val call_stack : unit -> callstack
val clear_call_stack : unit -> unit
Functions dealing with call stacks.
val pop_call_stack : unit -> unit
val push_call_stack : Cil_types.kernel_function -> Cil_types.kinstr -> unit
val current_kf : unit -> Kernel_function.t
The current function is the one on top of the call stack.
val call_stack : unit -> callstack
val pretty_call_stack_short : Format.formatter -> (Kernel_function.t * 'a) list -> unit
Print a call stack. The first one does not display the call sites.
val pretty_call_stack : Format.formatter -> (Kernel_function.t * Cil_types.kinstr) list -> unit
val pp_callstack : Format.formatter -> unit
Prints the current callstack.

Misc
val get_rounding_mode : unit -> Ival.Float_abstract.rounding_mode
val stop_if_stop_at_first_alarm_mode : unit -> unit

Assertions emitted during the analysis
val emitter : Emitter.t
val warn_all_mode : CilE.warn_mode
val with_alarm_stop_at_first : CilE.warn_mode
val with_alarms_raise_exn : exn -> CilE.warn_mode
val warn_all_quiet_mode : unit -> CilE.warn_mode
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
val set_loc : Cil_types.kinstr -> unit
module Got_Imprecise_Value: State_builder.Ref(Datatype.Bool)(sig
val name : string
val dependencies : State.t list
val default : unit -> bool
end)
val pretty_actuals : Format.formatter -> ('a * Cvalue.V.t * 'b) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
val warning_once_current : ('a, Format.formatter, unit) Pervasives.format -> 'a
val debug_result : Kernel_function.t ->
Cvalue.V_Offsetmap.t option * 'a * Base.SetLattice.t -> unit
val map_outputs : (Cvalue.Model.t -> 'a) ->
(Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list ->
(Cvalue.V_Offsetmap.t option * 'a) list
val remove_formals_from_state : Cil_types.varinfo list -> Cvalue.Model.t -> Cvalue.Model.t
module DegenerationPoints: Cil_state_builder.Stmt_hashtbl(Datatype.Bool)(sig
val name : string
val size : int
val dependencies : State.t list
end)
val warn_indeterminate : Kernel_function.t -> bool