diff --git a/tests/libc/check_some_metrics.sh b/tests/libc/check_some_metrics.sh new file mode 100755 index 0000000000000000000000000000000000000000..981a563580be0dbc279dc2bcef9f4f70f1092f67 --- /dev/null +++ b/tests/libc/check_some_metrics.sh @@ -0,0 +1,57 @@ +#!/usr/bin/env bash + +# Perform some checks on the output of the Metrics plugin, but avoiding +# too many details which cause conflicts during merge of libc branches. +# This test reads stdin and expects to find the output of 2 metrics runs: +# the first one with -metrics-libc and the second one with -metrics-no-libc. +# It then greps some lines and numbers, and check that their values are +# within specific conditions + +echo "Checking libc metrics..." + +regex=" *([a-zA-Z0-9\' -]+)+ +\(([0-9]+)\)" + +# tbl: stores mappings (<run>-<title>, <count>), where <run> is the +# metrics run (1 or 2), <title> is the Metrics title for the category, +# and <count> is the number between parentheses reported by Metrics. +declare -A tbl + +check () { # $1: state, $2: title, $3: expected cond + key="$1-$2" + count=${tbl[$key]} + test_exp='! [ $count $3 ]' + if eval $test_exp; then + echo "warning: [metrics run $state]: $2: expected $3, got $count" + fi +} + +# read stdin line by line and store relevant ones +# uses the '[metrics]' prefix to detect when a new run starts +state=0 +while IFS= read -r line; do + if [[ $line =~ "[metrics]" ]]; then + state=$((state + 1)) + fi + if [[ $line =~ $regex ]]; then + title="${BASH_REMATCH[1]}" + count=${BASH_REMATCH[2]} + tbl["$state-$title"]=$count + key="$state-$title" + fi +done + +# conditions to be checked + +check 1 "Defined functions" "> 100" +check 1 "Specified-only functions" "> 400" +check 1 "Undefined and unspecified functions" "< 2" +check 1 "'Extern' global variables" "> 20" +check 1 "Potential entry points" "= 1" + +check 2 "Defined functions" "= 1" +check 2 "Specified-only functions" "= 0" +check 2 "Undefined and unspecified functions" "= 0" +check 2 "'Extern' global variables" "= 0" +check 2 "Potential entry points" "= 1" + +echo "Finished checking libc metrics." diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 7c5a799d86a8dcb227925a5943141c9d2f532d1d..03409f942e69918252e3c02a8c8b2c1026508ddd 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -1,7 +1,8 @@ /* run.config* PLUGIN: @EVA_PLUGINS@ metrics + EXECNOW: BIN @PTEST_NAME@.sav @frama-c@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav MODULE: check_libc_naming_conventions, check_const - OPT: -print -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' -metrics -metrics-libc -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc + OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print MODULE: OPT: -print -print-libc -machdep x86_32 MODULE: check_parsing_individual_headers @@ -11,7 +12,8 @@ MODULE: check_compliance OPT: -kernel-msg-key printer:attrs MODULE: - CMD: %{dep:@PTEST_DIR@/check_full_libc.sh} @PTEST_SHARE_DIR@/libc + OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | ./check_some_metrics.sh + CMD: %{dep:./check_full_libc.sh} @PTEST_SHARE_DIR@/libc OPT: **/ #define __FC_REG_TEST diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle index 47563bc9e75736764af55207d61adb3fabeda9cb..96ad940d69778adf1aee7a90d46c4d25b63c46c2 100644 --- a/tests/libc/oracle/fc_libc.0.res.oracle +++ b/tests/libc/oracle/fc_libc.0.res.oracle @@ -1,231 +1,19 @@ +[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:170: assertion got status valid. -[eva] fc_libc.c:171: assertion got status valid. [eva] fc_libc.c:172: assertion got status valid. [eva] fc_libc.c:173: assertion got status valid. +[eva] fc_libc.c:174: assertion got status valid. +[eva] fc_libc.c:175: 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: -[metrics] Defined functions (129) - ======================= - Frama_C_abort (1 call); Frama_C_char_interval (1 call); - Frama_C_double_interval (0 call); Frama_C_float_interval (0 call); - Frama_C_interval (17 calls); Frama_C_make_unknown (6 calls); - Frama_C_nondet (13 calls); Frama_C_nondet_ptr (0 call); - Frama_C_update_entropy (7 calls); __FC_assert (7 calls); - __fc_atomic_compare_exchange_strong (3 calls); - __fc_atomic_compare_exchange_strong_explicit (0 call); - __fc_atomic_compare_exchange_weak (0 call); - __fc_atomic_compare_exchange_weak_explicit (0 call); - __fc_atomic_exchange (1 call); __fc_atomic_exchange_explicit (0 call); - __fc_atomic_fetch_add (1 call); __fc_atomic_fetch_add_explicit (0 call); - __fc_atomic_fetch_and (1 call); __fc_atomic_fetch_and_explicit (0 call); - __fc_atomic_fetch_or (1 call); __fc_atomic_fetch_or_explicit (0 call); - __fc_atomic_fetch_sub (1 call); __fc_atomic_fetch_sub_explicit (0 call); - __fc_atomic_fetch_xor (1 call); __fc_atomic_fetch_xor_explicit (0 call); - __fc_atomic_init_marker (0 call); __fc_atomic_is_lock_free (0 call); - __fc_atomic_load (1 call); __fc_atomic_load_explicit (0 call); - __fc_atomic_store_explicit_marker (0 call); - __fc_atomic_store_marker (0 call); __fc_initenv (4 calls); - __finite (0 call); __finitef (0 call); abs (0 call); argz_add (3 calls); - argz_add_sep (0 call); argz_append (2 calls); argz_count (0 call); - argz_create (0 call); argz_create_sep (0 call); argz_delete (0 call); - argz_extract (0 call); argz_insert (0 call); argz_next (1 call); - argz_replace (0 call); argz_stringify (0 call); asprintf (0 call); - atoi (0 call); atomic_flag_clear (0 call); - atomic_flag_clear_explicit (0 call); atomic_flag_test_and_set (0 call); - atomic_flag_test_and_set_explicit (0 call); atomic_signal_fence (0 call); - atomic_thread_fence (0 call); calloc (0 call); - canonicalize_file_name (0 call); char_equal_ignore_case (1 call); - fabs (0 call); fabsf (0 call); feholdexcept (0 call); fesetenv (0 call); - fetestexcept (0 call); getaddrinfo (0 call); getenv (0 call); - 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 (1 call); memcpy (7 calls); memmove (3 calls); - memoverlap (1 call); mempcpy (1 call); memrchr (0 call); memset (1 call); - posix_memalign (0 call); putenv (0 call); realpath (1 call); - res_search (1 call); setenv (0 call); setlocale (0 call); stpcpy (1 call); - str_append (3 calls); strcasecmp (0 call); strcat (0 call); - strchr (4 calls); strcmp (0 call); strcpy (1 call); strdup (0 call); - strerror (0 call); strlen (17 calls); strncat (0 call); strncmp (0 call); - strncpy (2 calls); strndup (1 call); strnlen (1 call); strrchr (0 call); - strsignal (0 call); strstr (2 calls); tolower (0 call); toupper (0 call); - unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcsdup (0 call); - wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call); - wmemset (0 call); - - Specified-only functions (429) - ============================== - 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); - Frama_C_long_long_interval (0 call); - 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); - Frama_C_unsigned_short_interval (0 call); _Exit (0 call); - __builtin_clz (0 call); __builtin_clzl (0 call); __builtin_clzll (0 call); - __builtin_ctz (0 call); __builtin_ctzl (0 call); __builtin_ctzll (0 call); - __builtin_popcount (0 call); __builtin_popcountl (0 call); - __builtin_popcountll (0 call); __builtin_sadd_overflow (0 call); - __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); - __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call); - __sync_synchronize (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); asctime (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); atan2l (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); - cfgetispeed (0 call); cfgetospeed (0 call); cfsetispeed (0 call); - cfsetospeed (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 (7 calls); - freeaddrinfo (0 call); freopen (0 call); frexp (0 call); frexpf (0 call); - frexpl (0 call); fseek (0 call); fseeko (0 call); fsetpos (0 call); - ftell (0 call); ftello (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); getsockname (0 call); getsockopt (0 call); - gettimeofday (0 call); getuid (0 call); gmtime (0 call); gmtime_r (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); ldexp (0 call); ldexpf (0 call); ldiv (0 call); - listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call); - localtime_r (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); lstat (0 call); malloc (13 calls); mblen (0 call); - mbstowcs (0 call); mbtowc (0 call); mkdir (0 call); mkfifo (0 call); - mknod (0 call); mkstemp (0 call); mkstemps (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_getname_np (0 call); pthread_join (0 call); - pthread_mutex_destroy (0 call); pthread_mutex_init (0 call); - pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); - pthread_mutexattr_destroy (0 call); pthread_mutexattr_init (0 call); - pthread_mutexattr_settype (0 call); pthread_setname_np (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 (7 calls); - recv (0 call); recvfrom (0 call); recvmsg (0 call); remove (0 call); - rename (0 call); rewind (0 call); round (0 call); roundf (0 call); - roundl (0 call); seed48 (0 call); select (0 call); send (0 call); - sendfile (0 call); sendto (0 call); setbuf (0 call); setegid (0 call); - seteuid (0 call); setgid (0 call); sethostname (0 call); setitimer (0 call); - setjmp (0 call); 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); settimeofday (0 call); setuid (0 call); - setvbuf (0 call); shutdown (0 call); 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); - sleep (0 call); socket (0 call); socketpair (0 call); sqrt (0 call); - sqrtf (0 call); sqrtl (0 call); srand (0 call); srand48 (0 call); - srandom (0 call); stat (0 call); strcasestr (0 call); strchrnul (0 call); - strcoll (0 call); strcspn (0 call); strftime (0 call); strlcat (0 call); - strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call); 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); - tan (0 call); tanf (0 call); tanl (0 call); tcflush (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); - uname (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); wcscasecmp (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); writev (0 call); - - Undefined and unspecified functions (1) - ======================================= - __builtin_abort (1 call); - - 'Extern' global variables (22) - ============================== - __fc_basename; __fc_dirname; __fc_fds; __fc_getpwuid_pw_dir; - __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; - __fc_heap_status; __fc_hostname; __fc_locale; __fc_locale_names; - __fc_mblen_state; __fc_mbtowc_state; __fc_random_counter; - __fc_socket_counter; __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg; - opterr; optopt; tzname - - Potential entry points (1) - ========================== - main; - - Global metrics - ============== - Sloc = 1649 - Decision point = 307 - Global variables = 86 - If = 292 - Loop = 55 - Goto = 118 - Assignment = 718 - Exit point = 129 - Function = 559 - Function call = 166 - Pointer dereferencing = 350 - Cyclomatic complexity = 436 [kernel] FRAMAC_SHARE/libc/sys/socket.h:451: Warning: clause with '\initialized' must contain name 'initialization' /* Generated by Frama-C */ @@ -322,37 +110,3 @@ void main(void) [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: -[metrics] Defined functions (1) - ===================== - main (0 call); - - Specified-only functions (0) - ============================ - - - Undefined and unspecified 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 diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..1bb2de127cd70bdff5ca432a89512ebb94cc355c --- /dev/null +++ b/tests/libc/oracle/fc_libc.5.res.oracle @@ -0,0 +1,2 @@ +Checking libc metrics... +Finished checking libc metrics.