Module Builtins_nonfree

module Builtins_nonfree: sig .. end
Non-free Value builtins. Contact CEA LIST for licensing

val register_builtin : string -> Db.Value.builtin_sig -> unit
val dkey : Log.category
exception Base_aligned_error
exception Found_misaligned_base
val frama_C_is_base_aligned : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
exception Offset_error
val frama_c_offset : Cvalue.Model.t ->
('a * Locations.Location_Bytes.t * 'b) list -> Value_types.call_result
exception Memcpy_result of Cvalue.Model.t
val frama_c_memcpy : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_copy_block : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_memset : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
exception Abort_to_top
val is_init : Cvalue.V_Or_Uninitialized.un_t -> bool
val singleton_eight : Ival.t
val abstract_strlen : max:Abstract_interp.Int.t ->
emit_alarm:(unit -> unit) ->
Locations.Location_Bytes.t -> Cvalue.Model.t -> Ival.t
val frama_c_strlen : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_strnlen : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val int_hrange : Abstract_interp.Int.t
val int_neg_ival : unit -> Ival.t
val int_pos_ival : unit -> Ival.t
val int_nonpos_ival : unit -> Ival.t
val int_nonneg_ival : unit -> Ival.t
val memcmp_ivals : Ival.t ->
Ival.t ->
Base.validity ->
Base.validity ->
Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.t -> int -> Cvalue.V.t
val frama_c_memcmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_interval_split : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val topify_pointed_arguments : Cvalue.Model.t ->
(Cil_types.exp * Locations.Location_Bytes.t * 'a) list -> Cvalue.Model.t
val frama_c_fscanf : Cvalue.Model.t ->
(Cil_types.exp * Locations.Location_Bytes.t * 'a) list ->
Value_types.call_result
val frama_c_ungarble : Cvalue.Model.t -> ('a * Cvalue.V.t * 'b) list -> Value_types.call_result
val _frama_c_va_nothing : string ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val _frama_c_va_arg : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result