From 20c65ae228621fbfcc720d3f39cd870a9d90b990 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 25 Jan 2022 22:27:53 +0100
Subject: [PATCH] [tests] prevent future conflicts in test oracle
---
tests/metrics/libc.c | 4 +-
tests/metrics/oracle/libc.1.res.oracle | 107 -------------------------
tests/metrics/oracle/libc.2.res.oracle | 1 -
tests/metrics/oracle/libc_metrics.err | 0
tests/metrics/oracle/libc_metrics.res | 4 +
5 files changed, 6 insertions(+), 110 deletions(-)
delete mode 100644 tests/metrics/oracle/libc.2.res.oracle
create mode 100644 tests/metrics/oracle/libc_metrics.err
create mode 100644 tests/metrics/oracle/libc_metrics.res
diff --git a/tests/metrics/libc.c b/tests/metrics/libc.c
index a753efa3828..80ddfacff98 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 dfcb77f3aee..1334ea6ba7f 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 1334ea6ba7f..00000000000
--- 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 00000000000..e69de29bb2d
diff --git a/tests/metrics/oracle/libc_metrics.res b/tests/metrics/oracle/libc_metrics.res
new file mode 100644
index 00000000000..bd056d31184
--- /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.
--
GitLab