module Builtins: sig
.. end
Analysis builtins for the cvalue domain, more efficient than the analysis
of the C functions. See for more details.
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type
builtin_type = unit -> Cil_types.typ * Cil_types.typ list
type
cacheable =
| |
Cacheable |
| |
NoCache |
| |
NoCacheCallers |
type
full_result = {
|
c_values : (Cvalue.V.t option * Cvalue.Model.t) list ; |
|
c_clobbered : Base.SetLattice.t ; |
|
c_from : (Function_Froms.froms * Locations.Zone.t) option ; |
}
type
call_result =
| |
States of Cvalue.Model.t list |
| |
Result of Cvalue.V.t list |
| |
Full of full_result |
type
builtin = Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t) list -> call_result
val register_builtin : string ->
?replace:string ->
?typ:builtin_type ->
cacheable -> builtin -> unit
val is_builtin : string -> bool