module Builtins: sig
.. end
Value analysis builtin shipped with Frama-C, more efficient than their
equivalent in C
exception Invalid_nb_of_args of int
val register_builtin : string -> ?replace: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 registered_builtins : unit -> (string * Db.Value.builtin_sig) list
Returns a list of the pairs (name, builtin_sig) registered via
register_builtin
.
Since Aluminium-20160501
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 find_builtin_override : Kernel_function.t -> Db.Value.builtin_sig option
Should the given function be replaced by a call to a builtin
val clobbered_set_from_ret : Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
clobbered_set_from_ret state ret
can be used for functions that return
a pointer to where they have written some data. It returns all the bases
of ret
whose contents may contain local variables.
val emit_alarm : kind:string -> text:string -> bool
Emit an ACSL assert (using \warning predicate) to signal that the
builtin encountered an alarm described by the string.
kind
is used to describe the alarm, similarly to Alarms.get_name
.
Identical alarms are not re-emitted. Returns true
iff it is a new alarm.
Change in Silicon-20161101: change return type
val fold_emitted_alarms : (Cil_types.stmt -> Cil_datatype.Code_annotation.Set.t -> 'a -> 'a) ->
'a -> 'a
Iteration on special assertions built by the builtins
val warn_definitions_overridden_by_builtins : unit -> unit
Emits warnings for each function definition that will be overridden by an
EVA built-in.
Does not include definitions in the Frama-C stdlib.
Since Phosphorus-20170501-beta1