sig
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
type cacheable = Eval.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 Builtins.full_result
type builtin =
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t) list -> Builtins.call_result
val register_builtin :
string ->
?replace:string ->
?typ:Builtins.builtin_type ->
Builtins.cacheable -> Builtins.builtin -> unit
val is_builtin : string -> bool
val prepare_builtins : unit -> unit
val is_builtin_overridden : Cil_types.kernel_function -> bool
val clobbered_set_from_ret :
Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue_domain.State.t
val find_builtin_override :
Cil_types.kernel_function ->
(string * Builtins.builtin * Builtins.cacheable * Cil_types.funspec)
option
val apply_builtin :
Builtins.builtin ->
Builtins.call ->
pre:Cvalue.Model.t -> post:Cvalue.Model.t -> Builtins.result list
end