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

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