Module Builtins_nonfree_print_c

module Builtins_nonfree_print_c: sig .. end
Translate a Value state into a bunch of C assertions

val substitute_space_by_underscore : string -> string
val c_string_of_int : Abstract_interp.Int.t -> string
val pretty_assignment_expression_ival : string -> Format.formatter -> Ival.t -> unit
val pretty_assignment_expression : string -> Format.formatter -> Locations.Location_Bytes.z -> unit
val pretty_int_range : Format.formatter -> (unit -> 'a) -> string -> string -> Cvalue.V.t -> unit
val pretty_int_assignment : Format.formatter -> string -> string -> Cvalue.V.t -> unit
val pretty_float_range : Format.formatter -> (unit -> 'a) -> string -> string -> Cvalue.V.t -> unit
val pretty_float_assignment : Format.formatter -> string -> string -> Cvalue.V.t -> unit
val pretty_pointer_assignment : Format.formatter -> string -> string -> Cvalue.V.t -> unit
val types : (int,
(Cvalue.V.t * string *
(Format.formatter ->
(unit -> unit) -> string -> string -> Cvalue.V.t -> unit) *
(Format.formatter -> string -> string -> Cvalue.V.t -> unit))
list)
Hashtbl.t
val value_pretty : bool ->
(unit -> unit) -> string -> int -> Format.formatter -> Cvalue.V.t -> unit
val value_uninit_pretty : bool ->
(unit -> unit) ->
string -> int -> Format.formatter -> Cvalue.V_Or_Uninitialized.un_t -> unit
val offsetmap_pretty : bool ->
string -> (unit -> unit) -> Format.formatter -> Cvalue.V_Offsetmap.t -> unit
val state_pretty : bool -> Format.formatter -> Cvalue.Model.tt -> unit
val pretty_state_as_c_assert : Format.formatter -> Cvalue.Model.t -> unit
val print_declarations_for_malloc_bases : Format.formatter -> unit
val pretty_state_as_c_assignments : Format.formatter -> Cvalue.Model.tt -> unit
val frama_c_dump_assert : Cvalue.Model.t -> 'a -> Value_types.call_result
val frama_c_dump_assignments : Cvalue.Model.t -> 'a -> Value_types.call_result