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 'frama-c -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;
}