module Builtins: sig
.. end
Value analysis builtin shipped with Frama-C, more efficient than their
equivalent in C
val table : (string, Db.Value.builtin_sig) Hashtbl.t
val register_builtin : string -> Db.Value.builtin_sig -> unit
Register the given OCaml function as a builtin, that will be used
instead of the Cil C function of the same name
val find_builtin : string -> Db.Value.builtin_sig
Find a previously registered builtin. Raises Not_found
if no such
builtin exists.
val mem_builtin : string -> bool
Does the builtin table contain an entry for name
?
val overridden_by_builtin : Value_parameters.BuiltinsOverrides.key -> bool
Should the given function be replaced by a call to a builtin
val type_from_nb_elems : loc:Cil_types.location ->
Cil_types.typ -> Abstract_interp.Int.t -> Cil_types.typ
Helper function to create the best type for a new base.
Builds an array type with the appropriate number of elements if needed
val double_double_fun : string ->
(Ival.Float_abstract.t -> Ival.Float_abstract.t) ->
Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val frama_C_cos : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_C_cos_precise : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_C_sin : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_C_sin_precise : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_C_compare_cos : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val float_or_double_fun_alarm : string ->
(Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t) ->
Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val register : string ->
(Ival.Float_abstract.rounding_mode ->
Ival.Float_abstract.t -> bool * Ival.Float_abstract.t) ->
unit
val frama_C_assert : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_bzero : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val dump_state : Cvalue.Model.t -> 'a -> Value_types.call_result
Builtins with multiple names; the lookup is done using a distinctive
prefix
module DumpFileCounters: State_builder.Hashtbl
(
Datatype.String.Hashtbl
)
(
Datatype.Int
)
(
sig
val size : int
val dependencies : State.t list
val name : string
end
)
val dump_state_file : string ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val dump_args : string ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result