module Builtins_nonfree_deterministic: sig
.. end
Non-free Value builtins for deterministic code.
Contact CEA LIST for licensing
exception Interpret_format_finished
exception Interpret_format_partial
exception Return_bottom
val bottom_result : Value_types.call_result
val alarm_behavior_raise_problem : CilE.alarm_behavior
val with_alarms : CilE.warn_mode
type
formatting_result = {
|
string : string ; |
|
partial : bool ; |
}
exception Copy_string_done
val copy_string : source_char_size:Abstract_interp.Int.t ->
Buffer.t -> Cvalue.Model.t -> Locations.Location_Bytes.t -> unit
val copy_char : Buffer.t -> Cvalue.V.t -> unit
val copy_int : modifier:'a -> hexa:bool -> Buffer.t -> Cvalue.V.t -> unit
val copy_pointer : modifier:'a -> Buffer.t -> Cvalue.V.t -> unit
val copy_float : modifier:'a -> Buffer.t -> Cvalue.V.t -> unit
val write_string_to_memory : Locations.Location_Bytes.t ->
Cvalue.Model.t ->
formatting_result -> Cvalue.Model.t
type
seen_percent =
val interpret_format : character_width:Abstract_interp.Int.t ->
Cvalue.Model.t ->
Locations.Location_Bytes.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list ->
formatting_result
val interpret_format_char : Cvalue.Model.t ->
Locations.Location_Bytes.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list ->
formatting_result
val interpret_format_wchar : Cvalue.Model.t ->
Locations.Location_Bytes.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list ->
formatting_result
val abstract_length : formatting_result -> Cvalue.V.t
val frama_c_printf : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_wprintf : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_sprintf : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result
val frama_c_snprintf : Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * 'a) list -> Value_types.call_result