Module Builtins

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.

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 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.