module Value_util:sig
..end
A call_stack is a list, telling which function was called at which
site. The head of the list tells about the latest call.
typecall_site =
Cil_types.kernel_function * Cil_types.kinstr
typecallstack =
call_site list
val call_stack : unit -> callstack
val clear_call_stack : unit -> unit
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
val call_stack : unit -> callstack
val pretty_call_stack_short : Format.formatter -> (Kernel_function.t * 'a) list -> unit
val pretty_call_stack : Format.formatter -> (Kernel_function.t * Cil_types.kinstr) list -> unit
val pp_callstack : Format.formatter -> unit
val get_rounding_mode : unit -> Ival.Float_abstract.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 : Value_parameters.SlevelFunction.key -> 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 -> (Cil_types.exp * Cvalue.V.t * 'a) 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: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.Set.elt -> bool
val register_new_var : Cil_types.varinfo -> Cil_types.typ -> unit
val create_new_var : string -> Cil_types.typ -> Cil_types.varinfo
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
-global-const
is set. In
this case, we forbid writing in a l-value that has this type.val float_kind : Cil_types.fkind -> Ival.Float_abstract.float_kind
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
class postconditions_mention_result :object
..end
\result
val postconditions_mention_result : ('a, Cil_types.identified_predicate, 'b) Cil_types.spec -> bool
\result
?val written_formals : WrittenFormals.key -> WrittenFormals.data
module WrittenFormals:Kernel_function.Make_Table
(
Datatype.List
(
Cil_datatype.Varinfo
)
)
(
sig
val size :int
val dependencies :State.t list
val name :string
end
)
val written_formals : WrittenFormals.key -> WrittenFormals.data