Module Builtins_nonfree_deterministic

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_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 = 
| Not_seen
| Seen of string * Integer.t option * Integer.t option * string * bool
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