diff --git a/tests/libc/check_some_metrics.sh b/tests/libc/check_some_metrics.sh index 981a563580be0dbc279dc2bcef9f4f70f1092f67..75e2282e30f33f7121824f196d86c290e6a997a3 100755 --- a/tests/libc/check_some_metrics.sh +++ b/tests/libc/check_some_metrics.sh @@ -2,13 +2,38 @@ # 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 +# +# This script expects a multiple of 5 arguments containing the expressions +# to compare for each 'run' of metrics: the first argument will be compared +# to the number of defined functions; the second argument to the number of +# specified functions; etc, until the 5th. Then, the 6th argument will +# correspond to the following run of metrics, until the 10th; and so on. +# +# This test reads stdin and expects to find the output of one or more metrics +# runs, which it then reads line by line, parses the relevant numbers, +# and compares them to the expressions passed as arguments. echo "Checking libc metrics..." +set -eu + +declare -A checks +runs=0 +cur_arg=0 +if [ $(($# % 5)) != 0 ]; then + echo "error: expected a multiple of 5 arguments, got $#" + exit 1 +fi +for ((run=1; run<=$(( ( $# ) / 5)); run++)) +do + for ((i=1;i<=5;i++)) + do + cur_arg=$((cur_arg+1)) + checks["${run}-$i"]="${!cur_arg}" + done + runs=$((runs+1)) +done + regex=" *([a-zA-Z0-9\' -]+)+ +\(([0-9]+)\)" # tbl: stores mappings (<run>-<title>, <count>), where <run> is the @@ -18,17 +43,19 @@ declare -A tbl check () { # $1: state, $2: title, $3: expected cond key="$1-$2" - count=${tbl[$key]} + count=${tbl[$key]-0} test_exp='! [ $count $3 ]' if eval $test_exp; then - echo "warning: [metrics run $state]: $2: expected $3, got $count" + echo "warning: [metrics run $1]: $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 +lines=0 while IFS= read -r line; do + lines=$((lines+1)) if [[ $line =~ "[metrics]" ]]; then state=$((state + 1)) fi @@ -36,22 +63,24 @@ while IFS= read -r line; do title="${BASH_REMATCH[1]}" count=${BASH_REMATCH[2]} tbl["$state-$title"]=$count - key="$state-$title" fi done +if [ "$state" == 0 ]; then + echo "error: no metrics output parsed." + exit 1 +fi + # 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" +for ((run=1; run<=$runs; run++)) +do + echo "Checking run $run..." + check $run "Defined functions" "${checks[$run-1]}" + check $run "Specified-only functions" "${checks[$run-2]}" + check $run "Undefined and unspecified functions" "${checks[$run-3]}" + check $run "'Extern' global variables" "${checks[$run-4]}" + check $run "Potential entry points" "${checks[$run-5]}" +done echo "Finished checking libc metrics." diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 03409f942e69918252e3c02a8c8b2c1026508ddd..c122ff2268ffa3f05bfb7a6677e4ca81e7b84ea2 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -1,6 +1,6 @@ /* 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 + EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav >@PTEST_NAME@_sav.res 2>@PTEST_NAME@_sav.err MODULE: check_libc_naming_conventions, check_const 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: @@ -12,7 +12,7 @@ MODULE: check_compliance OPT: -kernel-msg-key printer:attrs MODULE: - OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | ./check_some_metrics.sh + OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | ./check_some_metrics.sh "> 100" "> 400" "< 2" "> 20" "= 1" "= 1" "= 0" "= 0" "= 0" "= 1" CMD: %{dep:./check_full_libc.sh} @PTEST_SHARE_DIR@/libc OPT: **/ diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle index 1bb2de127cd70bdff5ca432a89512ebb94cc355c..bd056d31184ac4aa368a84cd783a7e683415b455 100644 --- a/tests/libc/oracle/fc_libc.5.res.oracle +++ b/tests/libc/oracle/fc_libc.5.res.oracle @@ -1,2 +1,4 @@ Checking libc metrics... +Checking run 1... +Checking run 2... Finished checking libc metrics. diff --git a/tests/libc/oracle/fc_libc_sav.err b/tests/libc/oracle/fc_libc_sav.err new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/libc/oracle/fc_libc_sav.res b/tests/libc/oracle/fc_libc_sav.res new file mode 100644 index 0000000000000000000000000000000000000000..6bfe1d501b92186f4b4283d9c3e9202294c1e834 --- /dev/null +++ b/tests/libc/oracle/fc_libc_sav.res @@ -0,0 +1 @@ +[kernel] Parsing fc_libc.c (with preprocessing) diff --git a/tests/metrics/libc.c b/tests/metrics/libc.c index a753efa3828153397a9cc8869a58261701ab5f20..80ddfacff9876941d852d5847b1d7cd40f4815dd 100644 --- a/tests/metrics/libc.c +++ b/tests/metrics/libc.c @@ -1,6 +1,6 @@ /* run.config - STDOPT: #"-metrics-no-libc -metrics-eva-cover" - STDOPT: #"-metrics-libc -metrics-eva-cover" + EXECNOW: LOG @PTEST_NAME@_metrics.res LOG @PTEST_NAME@_metrics.err @frama-c@ @PTEST_FILE@ -metrics -metrics-libc -then -metrics-no-libc | @PTEST_SUITE_DIR@/../libc/check_some_metrics.sh "> 5" "> 100" "= 0" "> 10" "= 2" "= 6" "= 0" "= 0" "= 0" "= 4" >@PTEST_NAME@_metrics.res 2>@PTEST_NAME@_metrics.err + STDOPT: #"-metrics-eva-cover" LOG: libc.json STDOPT: #"-metrics-libc -metrics-output @PTEST_RESULT@/libc.json" */ diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle index dfcb77f3aee0c8d35aebb3c99c7dcec1126c2dd6..1334ea6ba7f2ce1d2a266a2d45626085d55a8810 100644 --- a/tests/metrics/oracle/libc.1.res.oracle +++ b/tests/metrics/oracle/libc.1.res.oracle @@ -1,108 +1 @@ [kernel] Parsing libc.c (with preprocessing) -[metrics] Defined functions (7) - ===================== - bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call); - getopt (1 call); h (1 call); main (0 call); - - Specified-only functions (124) - ============================== - _exit (0 call); access (0 call); asprintf (0 call); chdir (0 call); - chown (0 call); chroot (0 call); clearerr (0 call); - clearerr_unlocked (0 call); close (0 call); dup (0 call); dup2 (0 call); - execl (0 call); execle (0 call); execlp (0 call); execv (0 call); - execve (0 call); execvp (0 call); fclose (0 call); fdopen (0 call); - feof (0 call); feof_unlocked (0 call); ferror (0 call); - ferror_unlocked (0 call); fflush (0 call); fgetc (0 call); fgetpos (0 call); - fgets (0 call); fileno (0 call); fileno_unlocked (0 call); - flockfile (0 call); fopen (0 call); fork (0 call); fputc (0 call); - fputs (0 call); fread (0 call); freopen (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); getc (0 call); - getc_unlocked (0 call); getchar (1 call); getchar_unlocked (0 call); - getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call); - gethostname (0 call); getopt_long (0 call); getopt_long_only (0 call); - getpgid (0 call); getpgrp (0 call); getpid (0 call); getppid (0 call); - getresgid (0 call); getresuid (0 call); gets (0 call); getsid (0 call); - getuid (0 call); isalnum (0 call); isalpha (1 call); isascii (0 call); - isatty (0 call); isblank (1 call); iscntrl (0 call); isdigit (0 call); - isgraph (0 call); islower (0 call); isprint (0 call); ispunct (0 call); - isspace (0 call); isupper (0 call); isxdigit (0 call); lseek (0 call); - pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call); - popen (0 call); putc (0 call); putc_unlocked (0 call); putchar (0 call); - putchar_unlocked (0 call); puts (0 call); read (0 call); remove (0 call); - rename (0 call); rewind (0 call); setbuf (0 call); setegid (0 call); - seteuid (0 call); setgid (0 call); sethostname (0 call); setpgid (0 call); - setregid (0 call); setresgid (0 call); setresuid (0 call); - setreuid (0 call); setsid (0 call); setuid (0 call); setvbuf (0 call); - sleep (0 call); sync (0 call); sysconf (0 call); tmpfile (0 call); - tmpnam (0 call); tolower (0 call); toupper (0 call); ttyname (0 call); - ungetc (0 call); unlink (0 call); usleep (0 call); vfprintf (0 call); - vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call); - vsprintf (0 call); write (0 call); - - Undefined and unspecified functions (0) - ======================================= - - - 'Extern' global variables (12) - ============================== - Frama_C_entropy_source; __fc_errno; __fc_fds; __fc_heap_status; - __fc_hostname; __fc_stdin; __fc_stdout; __fc_ttyname; optarg; opterr; - optind; optopt - - Potential entry points (2) - ========================== - f; main; - - Global metrics - ============== - Sloc = 20 - Decision point = 0 - Global variables = 18 - If = 0 - Loop = 0 - Goto = 0 - Assignment = 9 - Exit point = 7 - Function = 131 - Function call = 8 - Pointer dereferencing = 1 - Cyclomatic complexity = 7 -[eva] Analyzing a complete application starting at main -[eva] Computing initial state -[eva] Initial state computed -[eva:initial-state] Values of globals at initialization - fp ∈ {{ &g }} -[eva] using specification for function isalpha -[eva] using specification for function isblank -[eva] done for function main -[eva:summary] ====== ANALYSIS SUMMARY ====== - ---------------------------------------------------------------------------- - 5 functions analyzed (out of 6): 83% coverage. - In these functions, 13 statements reached (out of 13): 100% coverage. - ---------------------------------------------------------------------------- - No errors or warnings raised during the analysis. - ---------------------------------------------------------------------------- - 0 alarms generated by the analysis. - ---------------------------------------------------------------------------- - Evaluation of the logical properties reached by the analysis: - Assertions 0 valid 0 unknown 0 invalid 0 total - Preconditions 2 valid 0 unknown 0 invalid 2 total - 100% of the logical properties reached have been proven. - ---------------------------------------------------------------------------- -[metrics] Eva coverage statistics - ======================= - Syntactically reachable functions = 8 (out of 131) - Semantically reached functions = 8 - Coverage estimation = 100.0% -[metrics] References to non-analyzed functions - ------------------------------------ -[metrics] Statements analyzed by Eva - -------------------------- - 18 stmts in analyzed functions, 18 stmts analyzed (100.0%) - bar: 2 stmts out of 2 (100.0%) - foo: 2 stmts out of 2 (100.0%) - g: 2 stmts out of 2 (100.0%) - getopt: 5 stmts out of 5 (100.0%) - h: 2 stmts out of 2 (100.0%) - main: 5 stmts out of 5 (100.0%) diff --git a/tests/metrics/oracle/libc.2.res.oracle b/tests/metrics/oracle/libc.2.res.oracle deleted file mode 100644 index 1334ea6ba7f2ce1d2a266a2d45626085d55a8810..0000000000000000000000000000000000000000 --- a/tests/metrics/oracle/libc.2.res.oracle +++ /dev/null @@ -1 +0,0 @@ -[kernel] Parsing libc.c (with preprocessing) diff --git a/tests/metrics/oracle/libc_metrics.err b/tests/metrics/oracle/libc_metrics.err new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/metrics/oracle/libc_metrics.res b/tests/metrics/oracle/libc_metrics.res new file mode 100644 index 0000000000000000000000000000000000000000..bd056d31184ac4aa368a84cd783a7e683415b455 --- /dev/null +++ b/tests/metrics/oracle/libc_metrics.res @@ -0,0 +1,4 @@ +Checking libc metrics... +Checking run 1... +Checking run 2... +Finished checking libc metrics.