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