Skip to content
Snippets Groups Projects
Commit 20c65ae2 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] prevent future conflicts in test oracle

parent 2987c70e
No related branches found
No related tags found
No related merge requests found
/* run.config /* run.config
STDOPT: #"-metrics-no-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-libc -metrics-eva-cover" STDOPT: #"-metrics-eva-cover"
LOG: libc.json LOG: libc.json
STDOPT: #"-metrics-libc -metrics-output @PTEST_RESULT@/libc.json" STDOPT: #"-metrics-libc -metrics-output @PTEST_RESULT@/libc.json"
*/ */
......
[kernel] Parsing libc.c (with preprocessing) [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%)
[kernel] Parsing libc.c (with preprocessing)
Checking libc metrics...
Checking run 1...
Checking run 2...
Finished checking libc metrics.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment