Module Common.Charon_util

val size_of_int_ty : Charon.Values.int_ty -> int
val size_of_uint_ty : Charon.Values.u_int_ty -> int
val size_of_literal_ty : Charon.Types.literal_type -> int
val is_signed : Charon.Types.literal_type -> bool
val z_of_scalar : Charon.Values.scalar_value -> Soteria.Soteria_std.Z.t
val z_of_literal : Charon.Values.literal -> Soteria.Soteria_std.Z.t
val type_of_operand : Charon.Expressions.operand -> Charon.Types.ty
val lit_to_string : Charon.Types.literal_type -> string
val ty_as_float : Charon.Types.ty -> Charon.Values.float_type
val pp_literal_ty : Charon.Types.literal_type Fmt.t
val pp_ty : Charon.Types.ty Fmt.t
val lit_of_int_ty : Charon.Types.integer_type -> Charon.Types.literal_type
val lit_of_scalar : Charon.Values.scalar_value -> Charon.Types.literal_type
val lit_ty_of_lit : Charon.Values.literal -> Charon.Types.literal_type
val z_of_constant_expr : Charon.Types.constant_expr -> Soteria.Soteria_std.Z.t
val int_of_constant_expr : Charon.Types.constant_expr -> int
val field_tys : Charon.Types.field list -> Charon.Types.ty list
val empty_span_data : Charon.Meta.span_data
val empty_span : Charon.Meta.span
val fields_of_tys : Charon.Types.ty list -> Charon.Types.field list
val mk_array_ty : Charon.Types.ty -> Charon.Values.big_int -> Charon.Types.ty
val unit_ptr : Charon.Types.ty_kind

The type *const ()

val unit_ref : Charon.Types.ty_kind
val decl_has_attr : 'a Charon.GAst.gfun_decl -> string -> bool
val meta_get_attr : Charon.Types.item_meta -> string -> string option
val decl_get_attr : 'a Charon.GAst.gfun_decl -> string -> string option
val adt_is_box : Charon.Types.type_decl_ref -> bool
val adt_is_nonnull : Charon.Types.type_decl_ref -> bool
val get_pointee : Charon.Types.ty -> Charon.Types.ty
val float_precision : Charon.Values.float_type -> Soteria.Bv_values.Svalue.FloatPrecision.t
val ty_as_adt : Charon.Types.ty -> Charon.Types.type_decl_ref
val ty_is_monomorphic : Charon.Types.ty -> bool

Whether the given type is monomorphic, i.e. contains no type variables. This is a conservative estimate: struct Foo<T> {} is considered polymorphic despite the generics being unused.

val pp_span_data : Stdlib.Format.formatter -> Charon.Meta.span_data -> unit