[Kernel] improve message for absent compiler builtins

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

tests/syntax/compiler_builtins.c

+/* 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)
+}

tests/syntax/oracle/compiler_builtins.0.res.oracle

+[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;
+}
+
+

tests/syntax/oracle/compiler_builtins.1.res.oracle

+[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;
+}
+
+

tests/syntax/oracle/compiler_builtins.2.res.oracle

+[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;
+}
+
+