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.