sig
type call_site = Cil_types.kernel_function * Cil_types.kinstr
type callstack = Value_util.call_site list
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 -> Cil_types.kernel_function
val call_stack : unit -> Value_util.callstack
val pp_callstack : Format.formatter -> unit
val get_rounding_mode : unit -> Fval.rounding_mode
val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
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 alarm_report : ?level:int -> 'a Log.pretty_printer
module DegenerationPoints :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type key = Cil_types.stmt
type data = bool
val replace : key -> data -> unit
val add : key -> data -> unit
val clear : unit -> unit
val length : unit -> int
val iter : (key -> data -> unit) -> unit
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data
val find : key -> data
val find_all : key -> data list
val mem : key -> bool
val remove : key -> unit
end
val create_new_var : string -> Cil_types.typ -> Cil_types.varinfo
val is_const_write_invalid : Cil_types.typ -> bool
val float_kind : Cil_types.fkind -> Fval.float_kind
val postconditions_mention_result : Cil_types.funspec -> bool
val conv_comp : Cil_types.binop -> Abstract_interp.Comp.t
val conv_relation : Cil_types.relation -> Abstract_interp.Comp.t
val normalize_as_cond : Cil_types.exp -> bool -> Cil_types.exp
val is_value_zero : Cil_types.exp -> bool
val lval_to_exp : Cil_types.lval -> Cil_types.exp
val dump_garbled_mix : unit -> unit
val zone_of_expr :
(Cil_types.lval -> Precise_locs.precise_location) ->
Cil_types.exp -> Locations.Zone.t
val indirect_zone_of_lval :
(Cil_types.lval -> Precise_locs.precise_location) ->
Cil_types.lval -> Locations.Zone.t
end