Module Value_util

module Value_util: sig .. end

Callstacks related types and functions




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 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 -> Cil_types.kernel_function
The current function is the one on top of the call stack.
val call_stack : unit -> callstack
val pretty_call_stack_short : Format.formatter -> callstack -> unit
Print a call stack. The first one does not display the call sites.
val pretty_call_stack : Format.formatter -> callstack -> unit
val pp_callstack : Format.formatter -> unit
Prints the current callstack.

Others


val get_rounding_mode : unit -> Fval.rounding_mode
val stop_if_stop_at_first_alarm_mode : unit -> unit
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 warn_indeterminate : Kernel_function.t -> bool
val set_loc : Cil_types.kinstr -> unit
val pretty_actuals : Format.formatter -> (Cil_types.exp * 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
module DegenerationPoints: State_builder.Hashtbl  with type key = stmt and type data = bool
val create_new_var : string -> Cil_types.typ -> Cil_types.varinfo
Create and register a new variable inside Frama-C. The variable has its vlogic field set, meaning it is not a source variable. The freshness of the name must be ensured by the user.
val is_const_write_invalid : Cil_types.typ -> bool
Detect that the type is const, and that option -global-const is set. In this case, we forbid writing in a l-value that has this type.
val float_kind : Cil_types.fkind -> Fval.float_kind
Classify a Cil_types.fkind as either a 32 or 64 floating-point type. Emit a warning when the argument is long double, and long double is not equal to double
val postconditions_mention_result : Cil_types.funspec -> bool
Does the post-conditions of this specification mention \result?
val written_formals : Cil_types.kernel_function -> Cil_datatype.Varinfo.Set.t
Over-approximation of its formals the given function may write into.
val bind_block_locals : State_set.t -> Cil_types.block -> State_set.t
Bind all locals of the block to their default value (namely UNINITIALIZED)
val conv_comp : Cil_types.binop -> Abstract_interp.Comp.t
val conv_relation : Cil_types.relation -> Abstract_interp.Comp.t
val compatible_functions : with_alarms:CilE.warn_mode ->
Cil_types.varinfo -> Cil_types.typ -> Cil_types.typ -> bool
val zero : Cil_types.exp -> Cil_types.exp
Retun a zero constant compatible with the type of the argument
val is_value_zero : Cil_types.exp -> bool
Return true iff the argument has been created by Value_util.zero
val register_malloced_base : Base.t -> unit
These two functions are used to model the calls to malloc and free correctly.
val malloced_bases : unit -> Base.Hptset.t