diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 653febf25eb19fe0a24364f5d52a798a54a812a0..16b088b68fff25c7eddccdce038155a946c39eca 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -313,6 +313,15 @@ let in_ghost_block ?(battrs=[]) l =
get_statementloc (List.hd l),
get_statementloc (Extlib.last l)))
+let type_to_expr_for_builtin ~loc ~builtin specifier decl_type =
+ (* Prefix the builtin name with __fc_ to avoid collisions with real
+ world code. *)
+ let builtin = "__fc_" ^ builtin in
+ (* Build an expression representing the given type with a marker to indicate
+ the builtin for which this translation was made. *)
+ let info = SINGLE_INIT { expr_loc = loc; expr_node = VARIABLE builtin } in
+ { expr_loc = loc; expr_node = CAST ((specifier, decl_type), info) }
+
%}
%token <Filepath.position * string> SPEC
@@ -551,28 +560,31 @@ postfix_expression: /*(* 6.5.2 *)*/
| postfix_expression LPAREN arguments RPAREN ghost_arguments_opt
{ make_expr $sloc (CALL ($1, $3, $5))}
| BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN {
+ let builtin = "__builtin_va_arg" in
let b, d = $5 in
let loc = Cil_datatype.Location.of_lexing_loc $loc($5) in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
+ let type_as_expr = type_to_expr_for_builtin ~loc ~builtin b d in
make_expr $sloc
(CALL
({ expr_loc = loc_f;
- expr_node = VARIABLE "__builtin_va_arg"},
- [$3; { expr_loc = loc;
- expr_node = TYPE_SIZEOF (b, d)}],[]))
+ expr_node = VARIABLE builtin},
+ [$3; type_as_expr],[]))
}
| BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN {
+ let builtin = "__builtin_types_compatible_p" in
let b1,d1 = $3 in
let b2,d2 = $5 in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc1 = Cil_datatype.Location.of_lexing_loc $loc($3) in
let loc2 = Cil_datatype.Location.of_lexing_loc $loc($5) in
+ let type_as_expr1 = type_to_expr_for_builtin ~loc:loc1 ~builtin b1 d1 in
+ let type_as_expr2 = type_to_expr_for_builtin ~loc:loc2 ~builtin b2 d2 in
make_expr $sloc
(CALL
({expr_loc = loc_f;
- expr_node = VARIABLE "__builtin_types_compatible_p"},
- [ { expr_loc = loc1; expr_node = TYPE_SIZEOF(b1,d1)};
- { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
+ expr_node = VARIABLE builtin},
+ [ type_as_expr1; type_as_expr2],[]))
}
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN {
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2624f808f3295b20ddd30c873b30b3d85b310f27..8ca38fc5074160939c7b5a83a1ec2ce56d50cbc6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -260,7 +260,16 @@ let is_relational_bop = function
| EQ | NE | LT | GT | LE | GE -> true
| _ -> false
-let rec stripParen = function { expr_node = Cabs.PAREN e } -> stripParen e | e -> e
+let rec stripParen e =
+ match e with
+ | { expr_node = Cabs.PAREN e } -> stripParen e
+ | e -> e
+
+let is_for_builtin builtin info =
+ match info with
+ | SINGLE_INIT { expr_node = VARIABLE name } ->
+ String.equal ("__fc_" ^ builtin) name
+ | _ -> false
let rec is_dangerous_offset = function
NoOffset -> false
@@ -5815,6 +5824,26 @@ and doExp local_env
finishExp [] scope_chunk (new_exp ~loc (AlignOfE(e'')))
(Machine.sizeof_type ())
+ (* In cparser, the types used as arguments of certain builtins are converted
+ to casts so that they can be represented as expressions. The following
+ matches are special cases to type those expressions. They are then
+ converted to `sizeof typ` for CIL. *)
+ | Cabs.CAST ((specs, dt), info)
+ when is_for_builtin "__builtin_types_compatible_p" info ->
+ let typ = doOnlyType loc local_env.is_ghost specs dt in
+ let res = new_exp ~loc (SizeOf typ) in
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
+
+ | Cabs.CAST ((specs, dt), info)
+ when is_for_builtin "__builtin_va_arg" info ->
+ let typ = doOnlyType loc local_env.is_ghost specs dt in
+ if not (Cil.isCompleteType typ) then
+ Kernel.error ~current:true "__builtin_va_arg on incomplete type '%a'"
+ Cil_datatype.Typ.pretty typ;
+ let res = new_exp ~loc (SizeOf typ) in
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
+ (* End of special casts. *)
+
| Cabs.CAST ((specs, dt), ie) ->
let s', dt', ie' = preprocessCast loc local_env.is_ghost specs dt ie in
(* We know now that we can do s' and dt' many times *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index f3bc4b667c5897190f2def423642db64ac39e9ff..43115b0c53e02396d7d2eace0a01209c23cf7045 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1097,7 +1097,7 @@ class cil_printer () = object (self)
let last = self#getLastNamedArgument () in
self#instr fmt (Call(res,Cil.dummy_exp(Lval(Var vi,NoOffset)),[last],l))
- (* In cparser we have turned the call to
+ (* In cabs2cil we have turned the call to
__builtin_types_compatible_p(t1, t2) into
__builtin_types_compatible_p(sizeof t1, sizeof t2), so that we can
represent the types as expressions.
diff --git a/tests/syntax/builtin_types_compatible.i b/tests/syntax/builtin_types_compatible.i
new file mode 100644
index 0000000000000000000000000000000000000000..891cb5e7e4cc51d1f204b8e4f22cfced2fbc56bb
--- /dev/null
+++ b/tests/syntax/builtin_types_compatible.i
@@ -0,0 +1,6 @@
+/* run.config
+ OPT: -machdep gcc_x86_64 -print
+*/
+int main() {
+ return __builtin_types_compatible_p(int, int[]);
+}
diff --git a/tests/syntax/oracle/builtin_types_compatible.res.oracle b/tests/syntax/oracle/builtin_types_compatible.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..139913b6d02b7ab273e78c70b122d1ddad90dcdc
--- /dev/null
+++ b/tests/syntax/oracle/builtin_types_compatible.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing builtin_types_compatible.i (no preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+