Module Soteria_c_lib.Layout

module CF = Cerb_frontend
module BV = Typed.BitVec
module Agv = Aggregate_val
type bv_info = {
  1. bv_size : int;
  2. signed : bool;
}
type member_kind =
  1. | Padding of int
  2. | Field of Identifier.t
type layout = {
  1. size : int;
  2. align : int;
  3. members_ofs : (member_kind * int) list;
}
module Tag_defs : sig ... end
val is_int : CF.Ctype.ctype -> bool
val precision : CF.Ctype.floatingType -> Soteria.Bv_values.Svalue.FloatPrecision.t
val normalise_int_ty : Cerb_frontend.Ctype.integerType -> Cerb_frontend.Ctype.integerType
val size_of_int_ty : CF.Ctype.integerType -> int option
val align_of_int_ty : CF.Ctype.integerType -> int option
val size_of_float_ty : CF.Ctype.floatingType -> int option
val align_of_float_ty : CF.Ctype.floatingType -> int option
val size_of_int_ty_unsupported : CF.Ctype.integerType -> int Csymex.t
val get_array_info : CF.Ctype.ctype -> (CF.Ctype.ctype * Nat_big_num.num option) option
val get_struct_fields : CF.Symbol.sym -> ((Cerb_frontend.Symbol.identifier * (Cerb_frontend.Annot.attributes * CF.Ctype.alignment option * CF.Ctype.qualifiers * CF.Ctype.ctype)) list * CF.Ctype.flexible_array_member option) option
val get_struct_fields_ty : CF.Ctype.ctype -> ((Cerb_frontend.Symbol.identifier * (Cerb_frontend.Annot.attributes * CF.Ctype.alignment option * CF.Ctype.qualifiers * CF.Ctype.ctype)) list * CF.Ctype.flexible_array_member option) option
val layout_of : CF.Ctype.ctype -> layout option
val union_layout_of_members : (Identifier.t * (Cerb_frontend.Annot.attributes * CF.Ctype.alignment option * CF.Ctype.qualifiers * CF.Ctype.ctype)) list -> layout option
val layout_of_struct : Cerb_frontend.Symbol.sym -> layout option
val struct_layout_of_members : (Identifier.t * (Cerb_frontend.Annot.attributes * CF.Ctype.alignment option * CF.Ctype.qualifiers * CF.Ctype.ctype)) Soteria.Soteria_std.Foldable.List.t -> layout option

From: https://www.gnu.org/software/c-intro-and-ref/manual/html_node/Structure-Layout.html The structure’s fields appear in the structure layout in the order they are declared. When possible, consecutive fields occupy consecutive bytes within the structure. However, if a field’s type demands more alignment than it would get that way, C gives it the alignment it requires by leaving a gap after the previous field.

Once all the fields have been laid out, it is possible to determine the structure’s alignment and size. The structure’s alignment is the maximum alignment of any of the fields in it. Then the structure’s size is rounded up to a multiple of its alignment. That may require leaving a gap at the end of the structure.

val size_of_s : CF.Ctype.ctype -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t Csymex.t
val align_of_s : CF.Ctype.ctype -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t Csymex.t
val member_ofs : CF.Symbol.identifier -> CF.Ctype.ctype -> [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t Csymex.t
val is_int_ty_signed : CF.Ctype.integerType -> bool
val int_bv_info : CF.Ctype.integerType -> bv_info option
val bv_info : CF.Ctype.ctype -> bv_info option
val int_constraints : CF.Ctype.integerType -> ([< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t -> [> Soteria__Bv_values__Typed.sbool ] Soteria__Bv_values__Typed.t list) option
exception Unsupported of string
val constraints_exn : ty:CF.Ctype.ctype -> Agv.t -> Soteria_c_lib.Typed.T.sbool Typed.t list
val constraints : ty:CF.Ctype.ctype -> Agv.t -> Soteria_c_lib.Typed.T.sbool Typed.t list option
val nondet_c_ty_ : CF.Ctype.ctype_ -> Soteria_c_lib.Typed.T.cval Typed.t Csymex.t
val nondet_c_ty : CF.Ctype.ctype -> Soteria_c_lib.Typed.T.cval Typed.t Csymex.t
val nondet_c_ty_aggregate_ : CF.Ctype.ctype_ -> Agv.t Csymex.t
val nondet_c_ty_aggregate : CF.Ctype.ctype -> Agv.t Csymex.t
val int_ty_bounds : CF.Ctype.integerType -> (Soteria.Soteria_std.Z.t * Soteria.Soteria_std.Z.t) option
val type_conversion_arith : CF.Ctype.ctype -> CF.Ctype.ctype -> CF.Ctype.ctype

Returns the target type for "usual arithmetic conversions" between two types.

See https://learn.microsoft.com/en-us/cpp/c-language/usual-arithmetic-conversions

val c_int_size : int

Size of the int type in C.