fc_libc.0.res.oracle

[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[kernel] Parsing fc_libc.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva] fc_libc.c:209: assertion got status valid.
[eva] fc_libc.c:210: assertion got status valid.
[eva] fc_libc.c:211: assertion got status valid.
[eva] fc_libc.c:212: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_define_fd_set_t.h"
#include "__fc_define_timeval.h"
#include "__fc_gcc_builtins.h"
#include "__fc_integer.h"
#include "__fc_select.h"
#include "__fc_utmp_constants.h"
#include "alloca.h"
#include "argz.c"
#include "argz.h"
#include "assert.c"
#include "assert.h"
#include "ctype.c"
#include "ctype.h"
#include "dirent.h"
#include "err.h"
#include "errno.c"
#include "errno.h"
#include "error.c"
#include "error.h"
#include "fcntl.h"
#include "fenv.c"
#include "fenv.h"
#include "getopt.h"
#include "glob.c"
#include "glob.h"
#include "iconv.h"
#include "ifaddrs.h"
#include "inttypes.c"
#include "inttypes.h"
#include "libgen.h"
#include "locale.c"
#include "locale.h"
#include "math.c"
#include "math.h"
#include "netdb.c"
#include "netdb.h"
#include "netinet/in.h"
#include "poll.h"
#include "pthread.h"
#include "pwd.c"
#include "pwd.h"
#include "sched.h"
#include "semaphore.h"
#include "setjmp.h"
#include "signal.c"
#include "signal.h"
#include "spawn.h"
#include "stdarg.h"
#include "stdatomic.c"
#include "stdatomic.h"
#include "stddef.h"
#include "stdint.h"
#include "stdio.c"
#include "stdio.h"
#include "stdlib.c"
#include "stdlib.h"
#include "string.c"
#include "string.h"
#include "strings.h"
#include "stropts.h"
#include "sys/file.h"
#include "sys/resource.h"
#include "sys/select.h"
#include "sys/sendfile.h"
#include "sys/socket.c"
#include "sys/socket.h"
#include "sys/stat.h"
#include "sys/time.h"
#include "sys/times.h"
#include "sys/types.h"
#include "sys/uio.h"
#include "sys/utsname.h"
#include "sys/wait.h"
#include "syslog.h"
#include "termios.h"
#include "time.h"
#include "uchar.h"
#include "unistd.c"
#include "unistd.h"
#include "utmp.h"
#include "utmpx.h"
#include "wchar.c"
#include "wchar.h"
void main(void)
{
  /*@ assert __fc_p_fopen ≡ (FILE *)(&__fc_fopen); */ ;
  /*@ assert __fc_p_opendir ≡ (DIR *)(&__fc_opendir); */ ;
  /*@ assert __fc_p_time_tm ≡ &__fc_time_tm; */ ;
  /*@ assert __fc_p_strerror ≡ (char *)__fc_strerror; */ ;
  return;
}


[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: