fc_libc.0.res.oracle 13.2 KB
Newer Older
1 2 3 4 5 6
[kernel] Parsing tests/libc/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
  
Andre Maroneze's avatar
Andre Maroneze committed
7 8
[eva] tests/libc/fc_libc.c:153: assertion got status valid.
[eva] tests/libc/fc_libc.c:154: assertion got status valid.
9 10
[eva] tests/libc/fc_libc.c:155: assertion got status valid.
[eva] tests/libc/fc_libc.c:156: assertion got status valid.
11 12 13 14 15
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  
16
[metrics] Defined functions (82)
17
  ======================
18
   Frama_C_abort (1 call); Frama_C_char_interval (1 call);
19
   Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
20 21 22 23 24 25
   Frama_C_interval (14 calls); Frama_C_make_unknown (4 calls);
   Frama_C_nondet (12 calls); Frama_C_nondet_ptr (0 call);
   Frama_C_update_entropy (7 calls); __FC_assert (0 call);
   __fc_initenv (4 calls); __finite (0 call); __finitef (0 call); abs (0 call);
   atoi (0 call); calloc (0 call); char_equal_ignore_case (1 call);
   fabs (0 call); fabsf (0 call); feholdexcept (0 call); fesetenv (0 call);
26
   fetestexcept (0 call); getaddrinfo (0 call); getenv (0 call);
27 28 29 30 31 32
   gethostbyname (0 call); getline (0 call); glob (0 call); globfree (0 call);
   imaxabs (0 call); imaxdiv (0 call); isalnum (0 call); isalpha (0 call);
   isblank (0 call); iscntrl (0 call); isdigit (3 calls); isgraph (0 call);
   islower (0 call); isprint (0 call); ispunct (0 call); isspace (1 call);
   isupper (0 call); isxdigit (0 call); localeconv (0 call); main (0 call);
   memchr (0 call); memcmp (0 call); memcpy (4 calls); memmove (0 call);
33 34 35 36 37 38 39 40 41
   memoverlap (1 call); memrchr (0 call); memset (1 call);
   posix_memalign (0 call); putenv (0 call); res_search (1 call);
   setenv (0 call); setlocale (0 call); strcasecmp (0 call); strcat (0 call);
   strchr (3 calls); strcmp (0 call); strcpy (0 call); strdup (0 call);
   strerror (0 call); strlen (6 calls); strncat (0 call); strncmp (0 call);
   strncpy (2 calls); strndup (0 call); strnlen (0 call); strrchr (0 call);
   strsignal (0 call); strstr (0 call); tolower (0 call); toupper (0 call);
   unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
   wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call); 
42
  
David Bühler's avatar
David Bühler committed
43
  Undefined functions (384)
44 45 46
  =========================
   FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
   Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
47
   Frama_C_long_long_interval (0 call);
48 49 50 51 52
   Frama_C_real_interval_as_double (0 call); Frama_C_short_interval (0 call);
   Frama_C_size_t_interval (0 call); Frama_C_unsigned_char_interval (0 call);
   Frama_C_unsigned_int_interval (0 call);
   Frama_C_unsigned_long_interval (0 call);
   Frama_C_unsigned_long_long_interval (0 call);
53 54
   Frama_C_unsigned_short_interval (0 call); _Exit (0 call);
   __builtin_abort (1 call); __builtin_sadd_overflow (0 call);
55 56 57 58 59 60 61 62 63
   __builtin_saddl_overflow (0 call); __builtin_saddll_overflow (0 call);
   __builtin_smul_overflow (0 call); __builtin_smull_overflow (0 call);
   __builtin_smulll_overflow (0 call); __builtin_ssub_overflow (0 call);
   __builtin_ssubl_overflow (0 call); __builtin_ssubll_overflow (0 call);
   __builtin_uadd_overflow (0 call); __builtin_uaddl_overflow (0 call);
   __builtin_uaddll_overflow (0 call); __builtin_umul_overflow (0 call);
   __builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
   __builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
   __builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
David Bühler's avatar
David Bühler committed
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
   __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
   __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
   __va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
   __va_ioctl_void (0 call); __va_open_mode_t (0 call);
   __va_open_void (0 call); __va_openat_mode_t (0 call);
   __va_openat_void (0 call); _exit (0 call); abort (0 call); accept (0 call);
   access (0 call); acos (0 call); acosf (0 call); acosh (0 call);
   acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (0 call);
   asin (0 call); asinf (0 call); asinl (0 call); at_quick_exit (0 call);
   atan (0 call); atan2 (0 call); atan2f (0 call); atanf (0 call);
   atanl (0 call); atexit (0 call); atof (0 call); atol (0 call);
   atoll (0 call); basename (0 call); bind (0 call); bsearch (0 call);
   bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
   chdir (0 call); chown (0 call); chroot (0 call); clearerr (0 call);
   clearerr_unlocked (0 call); clock (0 call); clock_gettime (0 call);
   clock_nanosleep (0 call); close (0 call); closedir (0 call);
   closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
   cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
   dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
   dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
   execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
   exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
   fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
   ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
   fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
   fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
   floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
   fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
   fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
   freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
   ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
   gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
   getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
   getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
   getitimer (0 call); getopt (0 call); getopt_long (0 call);
   getopt_long_only (0 call); getpgid (0 call); getpgrp (0 call);
   getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
   getpwuid (0 call); getresgid (0 call); getresuid (0 call);
   getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
   getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
   gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
   iconv_close (0 call); iconv_open (0 call); inet_addr (2 calls);
   inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
   isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
   killpg (0 call); labs (0 call); lcong48 (0 call); ldiv (0 call);
   listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
   log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
   log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
   longjmp (0 call); lrand48 (0 call); lseek (0 call); malloc (7 calls);
   mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
   mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
   nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
   ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
   opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
   perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
   powf (0 call); pthread_cond_broadcast (0 call);
   pthread_cond_destroy (0 call); pthread_cond_init (0 call);
   pthread_cond_wait (0 call); pthread_create (0 call); pthread_join (0 call);
122 123 124 125 126 127 128
   pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
   pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
   putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
   puts (0 call); qsort (0 call); quick_exit (0 call); raise (0 call);
   rand (0 call); random (0 call); read (0 call); readdir (0 call);
   readv (0 call); realloc (3 calls); recv (0 call); recvmsg (0 call);
   remove (0 call); rename (0 call); rewind (0 call); round (0 call);
129 130 131
   roundf (0 call); roundl (0 call); seed48 (0 call); select (0 call);
   send (0 call); setbuf (0 call); setegid (0 call); seteuid (0 call);
   setgid (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
Andre Maroneze's avatar
Andre Maroneze committed
132 133 134
   setlogmask (0 call); setpgid (0 call); setpriority (0 call);
   setregid (0 call); setresgid (0 call); setresuid (0 call);
   setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
Andre Maroneze's avatar
Andre Maroneze committed
135
   settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
Andre Maroneze's avatar
Andre Maroneze committed
136 137 138 139 140
   sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
   sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
   siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
   sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
   sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
141 142 143
   srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
   strcasestr (0 call); strcoll (0 call); strcspn (0 call); strftime (0 call);
   strlcat (0 call); strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call);
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
   strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
   strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
   strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
   strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
   system (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
   truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
   umask (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
   utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
   vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
   wait (0 call); waitpid (0 call); wcschr (0 call); wcscmp (0 call);
   wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
   wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call);
   wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
   wmemmove (0 call); write (0 call); 
159
  
160
  'Extern' global variables (16)
161
  ==============================
Andre Maroneze's avatar
Andre Maroneze committed
162
   __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
Andre Maroneze's avatar
Andre Maroneze committed
163
   __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname; __fc_locale;
164 165
   __fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_wctomb_state;
   optarg; opterr; optopt; tzname
166 167 168 169 170 171 172
  
  Potential entry points (1)
  ==========================
   main; 
  
  Global metrics
  ============== 
173 174
  Sloc = 1083
  Decision point = 204
Andre Maroneze's avatar
Andre Maroneze committed
175
  Global variables = 70
176 177 178 179 180
  If = 195
  Loop = 43
  Goto = 89
  Assignment = 438
  Exit point = 82
David Bühler's avatar
David Bühler committed
181
  Function = 466
182 183 184
  Function call = 89
  Pointer dereferencing = 158
  Cyclomatic complexity = 286
185 186 187 188 189 190 191 192 193
/* Generated by Frama-C */
#include "__fc_builtin.c"
#include "__fc_builtin.h"
#include "__fc_define_fd_set_t.h"
#include "__fc_gcc_builtins.h"
#include "__fc_select.h"
#include "alloca.h"
#include "assert.c"
#include "assert.h"
194
#include "ctype.c"
195 196
#include "ctype.h"
#include "dirent.h"
197
#include "errno.c"
198 199 200 201
#include "errno.h"
#include "fcntl.h"
#include "fenv.c"
#include "fenv.h"
202
#include "getopt.c"
203
#include "getopt.h"
204
#include "glob.c"
205 206
#include "glob.h"
#include "iconv.h"
207
#include "inttypes.c"
208
#include "inttypes.h"
209
#include "libgen.h"
210 211 212 213 214 215
#include "locale.c"
#include "locale.h"
#include "math.c"
#include "math.h"
#include "netdb.c"
#include "netdb.h"
Andre Maroneze's avatar
Andre Maroneze committed
216
#include "netinet/in.h"
217 218 219 220
#include "poll.h"
#include "pthread.h"
#include "pwd.h"
#include "setjmp.h"
221
#include "signal.c"
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
#include "signal.h"
#include "stdarg.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/socket.h"
#include "sys/stat.h"
#include "sys/time.h"
#include "sys/times.h"
#include "sys/types.h"
#include "sys/uio.h"
#include "sys/wait.h"
#include "syslog.h"
#include "termios.h"
#include "time.h"
245
#include "unistd.c"
246
#include "unistd.h"
247
#include "wchar.c"
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
#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:
  
[metrics] Defined functions (1)
  =====================
   main (0 call); 
  
  Undefined functions (0)
  =======================
   
  
  'Extern' global variables (0)
  =============================
   
  
  Potential entry points (1)
  ==========================
   main; 
  
  Global metrics
  ============== 
  Sloc = 5
  Decision point = 0
  Global variables = 0
  If = 0
  Loop = 0
  Goto = 0
  Assignment = 0
  Exit point = 1
  Function = 1
  Function call = 0
  Pointer dereferencing = 0
  Cyclomatic complexity = 1