diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index ed8914b346ec1c47a40f6f8dbb8cf3c21b932e12..ef0d0d96c0390db868e258835bb64e7d59cdf16a 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1151,7 +1151,7 @@ and equalModuloPackedAlign attrs1 attrs2 =
Raises [Failure] if the fields are not equivalent.
If [mustCheckOffsets] is true, then there is already a difference in the
composite type, so each field must be checked. *)
-and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 =
+and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f1 f2 =
if f1.fbitfield <> f2.fbitfield then
raise (Failure "different bitfield info");
if mustCheckOffsets || not (equal_attributes_for_merge f1.fattr f2.fattr) then
@@ -1160,11 +1160,8 @@ and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 =
in which case the difference may be safely ignored *)
begin
try
- let offs1, width1 =
- Cil.bitsOffset typ_ci1 (Field (f1, NoOffset))
- in
- let offs2, width2 =
- Cil.bitsOffset typ_ci2 (Field (f2, NoOffset))
+ let offs1, width1 = Cil.fieldBitsOffset f1
+ and offs2, width2 = Cil.fieldBitsOffset f2
in
if not (equalModuloPackedAlign f1.fattr f2.fattr)
|| offs1 <> offs2 || width1 <> width2 then
@@ -1252,12 +1249,9 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
[%a] vs [%a]"
pp_attrs attrs pp_attrs oldattrs))
in
- let typ_ci = TComp(ci, {scache = Not_Computed}, []) in
- let typ_oldci = TComp(oldci, {scache = Not_Computed}, []) in
List.iter2
(fun oldf f ->
- checkFieldsEqualModuloPackedAlign ~mustCheckOffsets
- typ_ci typ_oldci f oldf;
+ checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
(* Make sure the types are compatible *)
(* Note: 6.2.7 §1 states that the names of the fields should be the
same. We do not force this for now, but could do it. *)
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index ce6b804ffac0b2a688bd0bdade62d83f9e640d84..0ed0755ee7f9f646292cc2f0ea738fcbf8f238d4 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -248,8 +248,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
try
let full_fields_to_print = List.fold_left
(fun acc field ->
- let current_offset = Field (field,NoOffset) in
- let start_o,width_o = bitsOffset typ current_offset in
+ let start_o,width_o = fieldBitsOffset field in
let start_o,width_o =
Integer.of_int start_o, Integer.of_int width_o
in
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index cc512a4d869da24ad9799974c91b3fd315a50cb0..50828024e849a3d79659f839306c2950c6aa85ac 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -433,13 +433,13 @@ and fieldinfo = {
expression. *)
mutable fsize_in_bits: int option;
- (** (Deprecated. Use {!Cil.bitsOffset} instead.) Similar to [fbitfield] for
- all types of fields.
+ (** (Deprecated. Use {!Cil.fieldBitsOffset} or {!Cil.bitsOffset} instead.)
+ Similar to [fbitfield] for all types of fields.
@deprecated only Jessie uses this *)
mutable foffset_in_bits: int option;
(** Offset at which the field starts in the structure. Do not read directly,
- but use {!Cil.bitsOffset} instead. *)
+ but use {!Cil.fieldBitsOffset} or {!Cil.bitsOffset} instead. *)
mutable fpadding_in_bits: int option;
(** (Deprecated.) Store the size of the padding that follows the field, if any.
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6567141ad0a51d2dbd1cff12ccae4751edb12368..30a1603c6ada298959263b39055535650a6e826c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1833,10 +1833,11 @@ class cil_printer () = object (self)
self#attributes fi.fattr;
if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then
try
- let (offset, size) = Cil.bitsOffset fi.ftype (Field (fi, NoOffset)) in
+ let (offset, size) = Cil.fieldBitsOffset fi in
let first = offset in
- let last = offset + size - 1 in
- fprintf fmt " /* bits %d .. %d */" first last
+ let last = if size > 0 then Some (offset + size - 1) else None in
+ let pp_opt fmt = Pretty_utils.pp_opt ~none:"" Format.pp_print_int fmt in
+ fprintf fmt " /* bits %d .. %a */" first pp_opt last
with Cil.SizeOfError _ -> ()
method private opt_funspec fmt funspec =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6f90ae11d735c7169a1ca90de6324221969f744b..f7bdda90abaa439fad1402a1d5e266322c403f1b 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4419,6 +4419,29 @@ and sizeOf ~loc t =
integer ~loc ((bitsSizeOf t) lsr 3)
with SizeOfError _ -> new_exp ~loc (SizeOf(t))
+and fieldBitsOffset (f : fieldinfo) : int * int =
+ if not f.fcomp.cstruct (* union *) then
+ 0, bitsSizeOf f.ftype
+ else begin
+ if f.foffset_in_bits = None then begin
+ let aux ~last acc fi =
+ let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
+ fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
+ fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
+ acc'
+ in
+ ignore (
+ fold_struct_fields aux
+ { oaFirstFree = 0;
+ oaLastFieldStart = 0;
+ oaLastFieldWidth = 0;
+ oaPrevBitPack = None }
+ f.fcomp.cfields
+ );
+ end;
+ Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
+ end
+
and bitsOffset (baset: typ) (off: offset) : int * int =
let rec loopOff (baset: typ) (width: int) (start: int) = function
NoOffset -> start, width
@@ -4432,38 +4455,13 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
let bitsbt = bitsSizeOf bt in
loopOff bt bitsbt (start + ei * bitsbt) off
end
- | Field(f, off) when not f.fcomp.cstruct (* union *) ->
+ | Field(f, off) ->
if check_invariants then
- assert (match unrollType baset with
- | TComp (ci, _, _) -> ci == f.fcomp
- | _ -> false);
+ (match unrollType baset with
+ | TComp (ci, _, _) -> assert (ci == f.fcomp)
+ | _ -> assert false);
+ let offsbits, size = fieldBitsOffset f in
(* All union fields start at offset 0 *)
- loopOff f.ftype (bitsSizeOf f.ftype) start off
-
- | Field(f, off) (* struct *) ->
- if check_invariants then
- assert (match unrollType baset with
- | TComp (ci, _, _) -> ci == f.fcomp
- | _ -> false);
- if f.foffset_in_bits = None then begin
- let aux ~last acc fi =
- let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
- fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
- fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
- acc'
- in
- ignore (
- fold_struct_fields aux
- { oaFirstFree = 0;
- oaLastFieldStart = 0;
- oaLastFieldWidth = 0;
- oaPrevBitPack = None }
- f.fcomp.cfields
- );
- end;
- let offsbits, size =
- Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
- in
loopOff f.ftype size (start + offsbits) off
in
loopOff baset (bitsSizeOf baset) 0 off
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 3bf916dcb66519cd830e6f6caaf5ab0d4d483d3f..60d2376a79df9ff31ac26fa6f68d96753423999d 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2185,6 +2185,13 @@ val intOfAttrparam: attrparam -> int option
* this after you call {!Cil.initCIL}. *)
val bitsOffset: typ -> offset -> int * int
+(** Give a field, returns the number of bits from the structure or union
+ * containing the field and the width (also expressed in bits) for the subobject
+ * denoted by the field. Raises {!Cil.SizeOfError} when it cannot compute
+ * the size. This function is architecture dependent, so you should only call
+ * this after you call {!Cil.initCIL}. *)
+val fieldBitsOffset: fieldinfo -> int * int
+
(** Like map but try not to make a copy of the list *)
val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 6d266b4f8a2cc85a28a4fffd1757128a5b45db9f..9f0e325e07c67523804413820be3da68a0b32379 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -470,10 +470,9 @@ let memset_typ_offsm_int full_typ i =
(* Do not produce NaN or infinites here (unless they are accepted
by the engine). *)
if Fval.is_finite f = True then update size v' else update size v
- | TComp ({ cstruct = true ; cfields = l}, _, _) as tcomp -> (* struct *)
+ | TComp ({ cstruct = true ; cfields = l}, _, _) -> (* struct *)
let aux_field offsm fi =
- let field = Field (fi, NoOffset) in
- let offset_fi = Int.of_int (fst (Cil.bitsOffset tcomp field)) in
+ let offset_fi = Int.of_int (fst (Cil.fieldBitsOffset fi)) in
aux fi.ftype (Int.add offset offset_fi) offsm
in
List.fold_left aux_field offsm l
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index b3893e9dc18e6b3dfc5a5623c1221f851f26176d..7844e81a2ceb93868468ff78f3e64ff7eb2d093f 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1250,7 +1250,7 @@ and eval_toffset ~alarm_mode env typ toffset =
| TField (fi, remaining) ->
let size_current default =
- try Ival.of_int (fst (Cil.bitsOffset typ (Field(fi, NoOffset))))
+ try Ival.of_int (fst (Cil.fieldBitsOffset fi))
with Cil.SizeOfError _ -> default
in
let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
diff --git a/src/plugins/value/values/main_locations.ml b/src/plugins/value/values/main_locations.ml
index 30069d98a9ef24037534ee12cdc43ccb1fa508d0..298f1b1698650bbc4b667439083ee6c96c211b04 100644
--- a/src/plugins/value/values/main_locations.ml
+++ b/src/plugins/value/values/main_locations.ml
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
-
module PLoc = struct
type value = Cvalue.V.t
@@ -70,10 +68,10 @@ module PLoc = struct
let no_offset = Precise Precise_locs.offset_zero
- let forward_field typ field = function
+ let forward_field _typ field = function
| Precise offset ->
begin try
- let field = fst (Cil.bitsOffset typ (Field (field, NoOffset))) in
+ let field = fst (Cil.fieldBitsOffset field) in
let field_i = Integer.of_int field in
Precise (Precise_locs.shift_offset_by_singleton field_i offset)
with Cil.SizeOfError _ -> Precise (Precise_locs.offset_top)
@@ -189,12 +187,12 @@ module PLoc = struct
then `Bottom
else `Value (new_mem, Precise new_off)
- let backward_field typ field = function
+ let backward_field _typ field = function
| Imprecise _ as x -> `Value x
| Precise offset ->
begin try
let offset_ival = Precise_locs.imprecise_offset offset in
- let field = fst (Cil.bitsOffset typ (Field (field, NoOffset))) in
+ let field = fst (Cil.fieldBitsOffset field) in
let field_i = Integer.of_int (- field) in
let ival = Ival.add_singleton_int field_i offset_ival in
if Ival.is_bottom ival
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index d1e8b5795328c83d795393ebc8b699a997b0749b..5615d0bd561ba28da9cc730684a02a61718cb383 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -99,15 +99,12 @@ struct
let typ = TComp(comp,Cil.empty_size_cache (),[]) in
H.add cache comp typ ; typ
- let field_offset cache fd =
- let typ = typ_of_comp cache fd.fcomp in
- let offset = Cil_types.(Field(fd,NoOffset)) in
- Cil.bitsOffset typ offset
+ let field_offset _cache fd =
+ Cil.fieldBitsOffset fd
let range_field cache fd =
let typ = typ_of_comp cache fd.fcomp in
- let offset = Cil_types.(Field(fd,NoOffset)) in
- Cil.bitsOffset typ offset , Cil.bitsSizeOf typ
+ Cil.fieldBitsOffset fd, Cil.bitsSizeOf typ
let range_index typ n =
let len = Cil.bitsSizeOf typ * n in (0 , len) , len
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 1511490737dca9c73d0586cd5b47119abeb27fab..cb2d079f01617cb9654a9320702f8fe1cab9adf9 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -489,12 +489,7 @@ let bits_sizeof_object = function
| C_array ainfo -> bits_sizeof_array ainfo
let field_offset fd =
- if fd.fcomp.cstruct then (* C struct *)
- let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
- let offset = Field(fd,NoOffset) in
- fst (Cil.bitsOffset ctype offset) / 8
- else (* CIL invariant: all C union fields start at offset 0 *)
- 0
+ fst (Cil.fieldBitsOffset fd) / 8
(* Conforms to C-ISO 6.3.1.8 *)
(* If same sign => greater rank. *)
diff --git a/tests/syntax/field-offsets.c b/tests/syntax/field-offsets.c
index dd972c8418ed4e042d4e2912312e7c538ea9599c..e29ff5e8e83a2e2cf667507ea5e185c214c54f8d 100644
--- a/tests/syntax/field-offsets.c
+++ b/tests/syntax/field-offsets.c
@@ -13,7 +13,7 @@ struct st {
struct fam {
int a;
char b;
- int fam[]; // check that a SizeOfError exception does not crash the printer
+ int fam[]; // check that the printer handles flexible arrays members
};
int main() {
diff --git a/tests/syntax/oracle/field-offsets.res.oracle b/tests/syntax/oracle/field-offsets.res.oracle
index 62a4b01b9fb855630e67033bd10a1a209ec595ba..f6ce77e05cea6fdf238ec7e97220c22ad40c6b87 100644
--- a/tests/syntax/oracle/field-offsets.res.oracle
+++ b/tests/syntax/oracle/field-offsets.res.oracle
@@ -9,7 +9,7 @@ struct st {
struct fam {
int a ; /* bits 0 .. 31 */
char b ; /* bits 32 .. 39 */
- int fam[] ;
+ int fam[] ; /* bits 64 .. */
};
int main(void)
{