diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 0363e6ffa8aa2cf372c856c446b81edac0630a94..195f318ade30738862a885f13ced8e4d800ae0a4 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -246,14 +246,29 @@ let () = Cmdline.run_after_exiting_stage run_list_all_plugin_options
(* Hooks independent from cmdline ordering *)
(**************************************************************************)
+
+
+let warn_if_another_compiler_builtin name =
+ try
+ let bt = Cil_builtins.Builtin_templates.find name in
+ let compiler = Option.get bt.compiler in
+ Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
+ ~current:true ~once:true
+ "%s is a compiler builtin, %s" name
+ (Cil.allowed_machdep (Cil_builtins.string_of_compiler compiler));
+ true
+ with Not_found -> false
+
(* This hook cannot be registered directly in Kernel or Cabs2cil, as it
depends on Ast_info *)
let on_call_to_undeclared_function vi =
let name = vi.Cil_types.vname in
- if not (Ast_info.is_frama_c_builtin name) then
- Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
- ~current:true ~once:true
- "Calling undeclared function %s. Old style K&R code?" name
+ if not (Ast_info.is_frama_c_builtin name) then begin
+ if not (warn_if_another_compiler_builtin name) then
+ Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
+ ~current:true ~once:true
+ "Calling undeclared function %s. Old style K&R code?" name
+ end
let () =
Cabs2cil.register_implicit_prototype_hook on_call_to_undeclared_function
diff --git a/tests/syntax/compiler_builtins.c b/tests/syntax/compiler_builtins.c
new file mode 100644
index 0000000000000000000000000000000000000000..175483a73c1cc5eea357932151b7e59e0e79d7d4
--- /dev/null
+++ b/tests/syntax/compiler_builtins.c
@@ -0,0 +1,28 @@
+/* run.config
+ STDOPT:
+ STDOPT: +"-machdep gcc_x86_32"
+ STDOPT: +"-machdep msvc_x86_64"
+ */
+
+#include <stdarg.h>
+
+struct st {
+ char a;
+ int b;
+};
+
+void fva(int a, ...) {
+ va_list ap;
+ __builtin_va_start(ap, a); // Non-MSVC-specific
+ __builtin_va_end(ap); // Non-MSVC-specific
+}
+
+int main() {
+ int x = 0;
+ if (__builtin_expect(x++, x)) { // GCC-specific
+ int y = x;
+ }
+ __builtin__annotation("a", 1); // MSVC-specific
+ fva(1);
+ __builtin_offsetof(struct st,b); // Generic builtin (always available)
+}
diff --git a/tests/syntax/oracle/compiler_builtins.0.res.oracle b/tests/syntax/oracle/compiler_builtins.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6c6a5186deee9987cd8db54445b900872bd973d3
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.0.res.oracle
@@ -0,0 +1,43 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin_va_end(__builtin_va_list); */
+/* compiler builtin:
+ void __builtin_va_start(__builtin_va_list); */
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+extern int ( /* missing proto */ __builtin__annotation)(char const *x_0,
+ int x_1);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if (tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/compiler_builtins.1.res.oracle b/tests/syntax/oracle/compiler_builtins.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0acfe18adc197fe809f31ac5a89e4ee723ad9d7c
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.1.res.oracle
@@ -0,0 +1,40 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin_va_end(__builtin_va_list); */
+/* compiler builtin:
+ void __builtin_va_start(__builtin_va_list); */
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+extern int ( /* missing proto */ __builtin__annotation)(char const *x_0,
+ int x_1);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if ((long)tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/compiler_builtins.2.res.oracle b/tests/syntax/oracle/compiler_builtins.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bdd362de6634afe39fca0b06a89f39de32e944e4
--- /dev/null
+++ b/tests/syntax/oracle/compiler_builtins.2.res.oracle
@@ -0,0 +1,45 @@
+[kernel] Parsing compiler_builtins.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:16: Warning:
+ __builtin_va_start is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:17: Warning:
+ __builtin_va_end is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
+/* Generated by Frama-C */
+#include "stdarg.h"
+/* compiler builtin:
+ void __builtin__annotation(...); */
+extern int ( /* missing proto */ __builtin_va_start)();
+
+extern int ( /* missing proto */ __builtin_va_end)(char *x_0);
+
+void fva(int a , ...)
+{
+ va_list ap;
+ __builtin_va_start(ap,a);
+ __builtin_va_end(ap);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ int x = 0;
+ ;
+ tmp = x;
+ x ++;
+ ;
+ if (tmp) {
+ int y = x;
+ }
+ __builtin__annotation("a",1);
+ fva(1);
+ __retres = 0;
+ return __retres;
+}
+
+