Skip to content
Snippets Groups Projects
Commit 2f9b5b70 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'fix/andre/libc-test-oracle' into 'master' 

[Libc] avoid merge conflicts in test oracle

See merge request frama-c/frama-c!3550
parents 0972d9a0 041900cb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 96 additions and 281 deletions
tests/libc/check_some_metrics.sh 0 → 100755
+ 57
− 0
View file @ 2f9b5b70
#!/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."
tests/libc/fc_libc.c
+ 4
− 2
View file @ 2f9b5b70
/* 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
......
tests/libc/oracle/fc_libc.0.res.oracle
+ 3
− 249
View file @ 2f9b5b70
[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
tests/libc/oracle/fc_libc.5.res.oracle 0 → 100644
+ 2
− 0
View file @ 2f9b5b70
Checking libc metrics...
Finished checking libc metrics.
tests/saveload/basic.i
+ 8
− 8
View file @ 2f9b5b70
/* run.config
MODULE: @PTEST_NAME@
EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/basic.sav > @PTEST_RESULT@/basic_sav.res 2> @PTEST_RESULT@/basic_sav.err
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
MODULE:
EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav @frama-c@ -save @PTEST_RESULT@/basic.1.sav @PTEST_FILE@ -eva @EVA_OPTIONS@ -out -input -deps > @PTEST_RESULT@/basic_sav.1.res 2> @PTEST_RESULT@/basic_sav.1.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.sav} -eva @EVA_OPTIONS@ -out -input -deps"
EXECNOW: BIN @PTEST_NAME@.1.sav LOG @PTEST_NAME@_sav.1.res LOG @PTEST_NAME@_sav.1.err @frama-c@ -save @PTEST_NAME@.1.sav @PTEST_FILE@ -eva @EVA_OPTIONS@ -out -input -deps > @PTEST_NAME@_sav.1.res 2> @PTEST_NAME@_sav.1.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps"
MODULE: @PTEST_NAME@
STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.1}.sav -eva @EVA_OPTIONS@ -out -input -deps -print"
STDOPT: +"-load %{dep:@PTEST_NAME@.1}.sav -eva @EVA_OPTIONS@ -out -input -deps -print"
MODULE:
STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.1}.sav -eva @EVA_OPTIONS@ -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_NAME@.1}.sav -eva @EVA_OPTIONS@ -out -input -deps"
MODULE: status
EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -save @PTEST_RESULT@/status.sav @PTEST_FILE@ > @PTEST_RESULT@/status_sav.res 2> @PTEST_RESULT@/status_sav.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/status.sav}"
EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -save status.sav @PTEST_FILE@ > status_sav.res 2> status_sav.err
STDOPT: +"-load %{dep:status.sav}"
MODULE:
STDOPT: +"-load %{dep:@PTEST_RESULT@/status.sav}"
STDOPT: +"-load %{dep:status.sav}"
*/
int main() {
int i,j; i=10; /*@ assert (i == 10); */
......
tests/saveload/bool.c
+ 3
− 3
View file @ 2f9b5b70
/* run.config
EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save @PTEST_RESULT@/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ %{dep:@PTEST_DIR@/bool.c} > @PTEST_RESULT@/bool_sav.res 2> @PTEST_RESULT@/bool_sav.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/bool.sav} -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_RESULT@/bool.sav} -eva @EVA_OPTIONS@"
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@"
*/
#include "stdbool.h"
......
tests/saveload/callbacks.i
+ 2
− 2
View file @ 2f9b5b70
/* run.config
EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ %{dep:@PTEST_DIR@/callbacks.i} -out -calldeps -eva-show-progress -main main1 -save @PTEST_RESULT@/callbacks.sav > @PTEST_RESULT@/callbacks_initial.res 2> @PTEST_RESULT@/callbacks_initial.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/callbacks.sav} -main main2 -then -main main3"
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ @PTEST_FILE@ -out -calldeps -eva-show-progress -main main1 -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3"
*/
/* This tests whether the callbacks for callwise inout and from survive after
......
tests/saveload/deps.i
+ 6
− 6
View file @ 2f9b5b70
/* run.config
MODULE: deps_A
EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/deps.sav > @PTEST_RESULT@/deps_sav.res 2> @PTEST_RESULT@/deps_sav.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -eva @EVA_OPTIONS@ -out -input -deps "
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps "
MODULE: deps_B
STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps "
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps "
MODULE: deps_C
STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps "
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps "
MODULE: deps_D
STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps "
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps "
MODULE: deps_E
STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps "
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps "
*/
int main() {
......
tests/saveload/isset.c
+ 5
− 5
View file @ 2f9b5b70
/* run.config
EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_RESULT@/isset.sav %{dep:@PTEST_DIR@/isset.c} > @PTEST_RESULT@/isset_sav.res 2> @PTEST_RESULT@/isset_sav.err
STDOPT: +"-quiet -load %{dep:@PTEST_RESULT@/isset.sav}"
STDOPT: +"-load %{dep:@PTEST_RESULT@/isset.sav}"
STDOPT: +"-eva @EVA_OPTIONS@ -load %{dep:@PTEST_RESULT@/isset.sav}"
STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load %{dep:@PTEST_RESULT@/isset.sav}"
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_NAME@.sav @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-quiet -load %{dep:@PTEST_NAME@.sav}"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
STDOPT: +"-eva @EVA_OPTIONS@ -load %{dep:@PTEST_NAME@.sav}"
STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load %{dep:@PTEST_NAME@.sav}"
*/
int main() {
......
tests/saveload/multi_project.i
+ 2
− 2
View file @ 2f9b5b70
/* run.config
PLUGIN: @EVA_PLUGINS@ constant_propagation
EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err @frama-c@ -save @PTEST_RESULT@/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_RESULT@/multi_project_sav.res 2> @PTEST_RESULT@/multi_project_sav.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/multi_project.sav}"
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
MODULE: @PTEST_NAME@
OPT: -eva @EVA_OPTIONS@
*/
......
tests/saveload/segfault_datatypes.i
+ 2
− 2
View file @ 2f9b5b70
/* run.config*
MODULE: segfault_datatypes_A
EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/segfault_datatypes.sav > @PTEST_RESULT@/segfault_datatypes_sav.res 2> @PTEST_RESULT@/segfault_datatypes_sav.err
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
MODULE: segfault_datatypes_B
STDOPT: +"-load %{dep:@PTEST_RESULT@/segfault_datatypes.sav} -eva -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva -out -input -deps"
*/
int main() {
......
tests/saveload/sparecode.i
+ 2
− 2
View file @ 2f9b5b70
/* run.config
PLUGIN: @EVA_PLUGINS@ slicing
EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save @PTEST_RESULT@/sparecode.sav %{dep:@PTEST_DIR@/sparecode.i} -then-on 'Slicing export' -print > @PTEST_RESULT@/sparecode_sav.res 2> @PTEST_RESULT@/sparecode_sav.err
STDOPT: +"-load %{dep:@PTEST_RESULT@/sparecode.sav}"
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save @PTEST_NAME@.sav @PTEST_FILE@ -then-on 'Slicing export' -print > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
*/
int G;
int f (int x, int y) {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment