Module Builtins_nonfree

module Builtins_nonfree: sig .. end
Implementation of memset that accepts imprecise arguments. Assumes the syntactic context is positioned.

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 two61 : Integer.t
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_imprecise : Cvalue.Model.t ->
Locations.Location_Bytes.t ->
Cvalue.V.t -> Cvalue.V.t -> Value_types.call_result
Implementation of memset that accepts imprecise arguments. Assumes the syntactic context is positioned.
type imprecise_memset_reason = 
| UnsupportedType
| ImpreciseTypeSize
| NoTypeForDest
| NotSingletonLoc
| SizeMismatch
| ImpreciseValue
| ImpreciseSize
| NegativeOrNullSize
exception ImpreciseMemset of imprecise_memset_reason
val pretty_imprecise_memset_reason : Format.formatter -> imprecise_memset_reason -> unit
val memset_typ_offsm_int : Cil_types.typ -> Abstract_interp.Int.t -> Cvalue.V_Offsetmap.t
memset_typ_offsm typ i returns an offsetmap of size sizeof(typ) that maps each byte to the integer i. The shape of the type is respected: the fields in typ are bound to values of the good type, not just to 'i%repeated modulo 8'. May raise ImpreciseMemset.
val memset_typ_offsm : Cil_types.typ -> Cvalue.V.t -> Cvalue.V_Offsetmap.t
Type-aware memset on an entire type. Same as memset_typ_offsm_int, but with a Cvalue.V instead of an integer. We accept -ilevel different possible values in v before falling back to the imprecise memset. May rais Builtins_nonfree.ImpreciseMemset.
val frama_c_memset_precise : Cvalue.Model.t ->
Locations.Location_Bytes.t ->
Cvalue.V.t -> Cil_types.exp * Cvalue.V.t -> Value_types.call_result
Precise memset builtin, that requires its arguments to be sufficiently precise abstract values. Assumes the syntactic context is positioned.
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.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 ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val abstract_strcmp : size:Abstract_interp.Int.t ->
signed:bool ->
min:Abstract_interp.Int.t ->
max:Abstract_interp.Int.t ->
emit_alarm:('a -> unit) ->
Locations.Location_Bytes.t ->
'a -> Locations.Location_Bytes.t -> 'a -> Cvalue.Model.t -> Ival.t
val frama_c_strcmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_c_wcscmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_strcmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_c_strncmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
val frama_c_wcsncmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_strncmp : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) 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 ->
[< `Bottom | `Map of Cvalue.V_Offsetmap.t | `Top ] ->
[< `Bottom | `Map of Cvalue.V_Offsetmap.t | `Top ] -> 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 ->
(Cil_types.exp * Cvalue.V.t * 'a) 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