diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 666053a2830b8b449ef19dc859732f997842f7bc..fadfd5c594962dfe9001468527a4479483bf3c7d 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -566,7 +566,14 @@ postfix_expression: /*(* 6.5.2 *)*/
{ expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
}
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN
- { transformOffsetOf $3 $5 }
+ {
+ let loc_f = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
+ let arg = transformOffsetOf $3 $5 in
+ let builtin = { expr_loc = loc_f;
+ expr_node = VARIABLE "__builtin_offsetof" }
+ in
+ make_expr (CALL (builtin, [ arg ], []))
+ }
| postfix_expression DOT id_or_typename { make_expr (MEMBEROF ($1, $3))}
| postfix_expression ARROW id_or_typename { make_expr (MEMBEROFPTR ($1, $3)) }
| postfix_expression PLUS_PLUS { make_expr (UNARY (POSINCR, $1)) }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 42b88e95e867c4fef0baf76a19e551bce5c492e5..39a07c2eb0efeccf0f203730e413bdc06440baaf 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7026,6 +7026,28 @@ and doExp local_env
Kernel.warning ~current:true
"Invalid call to builtin_constant_p")
end
+ | "__builtin_offsetof" ->
+ begin
+ match !pargs with
+ | [{ enode = CastE (_, {enode = AddrOf (host, offset)}) } as e] ->
+ begin
+ piscall := false;
+ prestype := Cil.theMachine.Cil.typeOfSizeOf;
+ try
+ let typ = Cil.typeOfLhost host in
+ let start, _width = Cil.bitsOffset typ offset in
+ if start mod 8 <> 0 then
+ Kernel.error ~current:true "Using offset of bitfield";
+ let kind = Cil.theMachine.kindOfSizeOf in
+ pres := Cil.kinteger ~loc:e.eloc kind (start / 8);
+ with SizeOfError _ ->
+ pres := e;
+ Kernel.warning ~once:true ~current:true
+ "Invalid call to builtin_offsetof";
+ end
+ | _ ->
+ Kernel.abort ~current:true "Invalid call to builtin_offsetof";
+ end
| "__builtin_types_compatible_p" ->
begin
(* Constant-fold the argument and see if it is a constant *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index aef5019984374c17ebe290473bdad37498ef234e..8bb7a5f20ef2b90a758f0512cb0fa2b1734a4c37 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1047,6 +1047,23 @@ class cil_printer () = object (self)
"__builtin_types_compatible_p: cabs2cil should have added sizeof to \
the arguments."
+ | Call(dest, {enode = Lval (Var vi, NoOffset)}, [ arg ], (l, _))
+ when vi.vname = "__builtin_offsetof"
+ && not state.print_cil_as_is ->
+ begin
+ match arg.enode with
+ | CastE (_, { enode = AddrOf (host, offset) }) ->
+ (* Print the destination *)
+ Extlib.may (fprintf fmt "%a = " self#lval) dest;
+ (* Now the call itself *)
+ fprintf fmt "%a(%a, %a)%s"
+ self#varname vi.vname
+ (self#typ None) (Cil.typeOfLhost host)
+ self#offset offset
+ instr_terminator
+ | _ -> Kernel.fatal ~source:l "__builtin_offsetof: invalid argument."
+ end
+
| Call(dest,e,args,_) -> pp_call dest e fmt args
| Asm(attrs, tmpls, ext_asm, l) ->
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 459570e1be633a25dff4695a87a15ca68b8d94fe..91afc7abef7cb35dba23486b61d98c8d8a617bc4 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4509,19 +4509,6 @@ and constFold (machdep: bool) (e: exp) : exp =
| AlignOfE _ | AlignOf _ | SizeOfStr _ | SizeOfE _ | SizeOf _ ->
e (* Depends on machdep. Do not evaluate in this case*)
- (* Special case to handle the C macro 'offsetof' *)
- | CastE(it,
- { enode = AddrOf (Mem ({enode = CastE(TPtr(bt, _), z)}), off)})
- when machdep && isZero z -> begin
- try
- let start, _width = bitsOffset bt off in
- if start mod 8 <> 0 then
- Kernel.error ~current:true "Using offset of bitfield" ;
- constFold machdep
- (new_exp ~loc (CastE(it, (integer ~loc (start / 8)))))
- with SizeOfError _ -> e
- end
-
| CastE (t, e) -> begin
Kernel.debug ~dkey "ConstFold CAST to %a@." !pp_typ_ref t ;
let e = constFold machdep e in
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index 8688b345c3b3594eeea05def8b5272705946c351..f3f41b911f79f21e9366a965bfe0aa12ef6c231f 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -87,6 +87,8 @@
adding aligned(1) attribute to field 'PACKOVERPOP.j' due to packing pragma
[kernel:typing:pragma] tests/misc/pragma-pack.c:88:
adding aligned(1) attribute to comp 'PACKOVERPOP' due to packing pragma
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[kernel:typing:pragma] tests/misc/pragma-pack.c:133:
packing pragma: restoring alignment to default (16)
[kernel:typing:pragma] tests/misc/pragma-pack.c:135:
diff --git a/tests/misc/oracle/pragma-pack.1.res.oracle b/tests/misc/oracle/pragma-pack.1.res.oracle
index 559d8cfaacbfa9512139f9d2ffe64db5ba5cbe8e..59c543748f2670f2d4076cc9e89d80dbf6399971 100644
--- a/tests/misc/oracle/pragma-pack.1.res.oracle
+++ b/tests/misc/oracle/pragma-pack.1.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma-pack.c (with preprocessing)
[kernel] tests/misc/pragma-pack.c:87: Warning:
ignoring #pragma pack(pop) with empty stack
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma-pack.2.res.oracle b/tests/misc/oracle/pragma-pack.2.res.oracle
index ae56a3d1f1afeff64dfbe4883fe7954bcfffc7e8..c2534c76f82ba9a71c3e97f89c3448eb8838d4cc 100644
--- a/tests/misc/oracle/pragma-pack.2.res.oracle
+++ b/tests/misc/oracle/pragma-pack.2.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma-pack.c (with preprocessing)
[kernel] tests/misc/pragma-pack.c:87: Warning:
ignoring #pragma pack(pop) with empty stack
+[kernel:typing:implicit-function-declaration] tests/misc/pragma-pack.c:104: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma_pack_zero.0.res.oracle b/tests/misc/oracle/pragma_pack_zero.0.res.oracle
index 6c491d9c591bde8b39ace7f8457e34dabd4a15c3..0137611438a4097652781738f9ee7c3ea0bb2d59 100644
--- a/tests/misc/oracle/pragma_pack_zero.0.res.oracle
+++ b/tests/misc/oracle/pragma_pack_zero.0.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma_pack_zero.c (with preprocessing)
[kernel] tests/misc/pragma_pack_zero.c:35: Warning:
GCC accepts pack(0) but does not specify its behavior; considering it equivalent to pack()
+[kernel:typing:implicit-function-declaration] tests/misc/pragma_pack_zero.c:47: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/misc/oracle/pragma_pack_zero.1.res.oracle b/tests/misc/oracle/pragma_pack_zero.1.res.oracle
index 69b3a971800c05c4f0d209e3e1588e097af670b4..672ee382233f825a45eb7b43387c5009b13ab2c3 100644
--- a/tests/misc/oracle/pragma_pack_zero.1.res.oracle
+++ b/tests/misc/oracle/pragma_pack_zero.1.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/misc/pragma_pack_zero.c (with preprocessing)
[kernel] tests/misc/pragma_pack_zero.c:35: Warning:
ignoring invalid packing alignment (0)
+[kernel:typing:implicit-function-declaration] tests/misc/pragma_pack_zero.c:47: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/syntax/oracle/offsetof.res.oracle b/tests/syntax/oracle/offsetof.res.oracle
index ac9886f97c2ae844c60f2ab7e83ba27da8464b48..0829a102008ff37c8af5670f4ae9ae58a26e6164 100644
--- a/tests/syntax/oracle/offsetof.res.oracle
+++ b/tests/syntax/oracle/offsetof.res.oracle
@@ -1,13 +1,12 @@
[kernel] Parsing tests/syntax/offsetof.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/syntax/offsetof.c:6: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
/* Generated by Frama-C */
#include "stddef.h"
-struct c {
- char ca ;
-};
void main(void)
{
size_t S;
- S = (unsigned int)(& ((struct c *)0)->ca);
+ S = 0U;
return;
}
diff --git a/tests/value/oracle/attribute-aligned.res.oracle b/tests/value/oracle/attribute-aligned.res.oracle
index c451f494f10d20216b94e1311cafe4973155636d..160214c6a77d36c669f86508fef2ea0f157af179 100644
--- a/tests/value/oracle/attribute-aligned.res.oracle
+++ b/tests/value/oracle/attribute-aligned.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/value/attribute-aligned.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/value/attribute-aligned.c:17: Warning:
+ Calling undeclared function __builtin_offsetof. Old style K&R code?
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed