diff --git a/Makefile b/Makefile
index 9bd6c09c37124287858bfa2b92926d5c3dfaca7b..077e549924b8f5aa008661d80e2f897c7d00eae2 100644
--- a/Makefile
+++ b/Makefile
@@ -170,12 +170,10 @@ force-reconfigure:
# todo: adds bugs?
# todo: adds crowbar?
-# todo: adds dynamic?
# todo: adds dynamic_plugin?
# todo: adds fc_script
# todo: adds make_run_script
# todo: adds more_wp
-# todo: adds pretty_printing: fixes tests/pretty_printing/ghost_parameters.c
# todo: adds saveload
# todo: adds value/numerors? (requires opam package mlgmpidl and system libraries for MPFR)
# todo: adds verisec
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 3735bdaad1e99df46d82f31321d33ab0339913ba..7cc8be13f10d51f357be5f3f5ffed59a5b8392fb 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -978,10 +978,10 @@ let get_macros cmd =
Macros.add_list macros cmd.macros
let contains_frama_c_binary_name =
- Str.regexp "[^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c\\).*"
+ Str.regexp "\\([^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c\\)\\(\\.opt\\|\\.byte\\|\\.exe\\)?\\($\\|[ \t]\\)\\)"
let frama_c_binary_name =
- Str.regexp "\\([^ ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c\\)\\(\\.opt\\|\\.byte\\|\\.exe\\)?\\)"
+ Str.regexp "\\([^( ]*\\(toplevel\\|viewer\\|frama-c-gui\\|frama-c\\)\\(\\.opt\\|\\.byte\\|\\.exe\\)?\\)"
let basic_command_string =
fun command ->
diff --git a/src/plugins/report/.gitignore b/src/plugins/report/.gitignore
index 0c1cd282dd0ab82298b5854b22dc24b8f6cd8e8b..3a98458e917cbf63ae42a311989dbe7be4a5d56c 100644
--- a/src/plugins/report/.gitignore
+++ b/src/plugins/report/.gitignore
@@ -1,5 +1,4 @@
/configure
/Makefile
-/tests/ptests_config
/tests/*/result
/tests/**/dune
diff --git a/src/plugins/report/tests/ptests_config b/src/plugins/report/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..2af08cc747973c537e3aff87ee963b13852a0d95
--- /dev/null
+++ b/src/plugins/report/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= report
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index bc22ab8755cb229511540c6e520266175328e2ad..99e9a5a94e320b377ce9179da25d25cab2b6b3d9 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,11 +1,12 @@
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
+ DEPS: for-find-fun2.c for-find-fun.c main2.c main3.c
EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= frama-c-script make-template . < %{dep:make_template.input} > make_template.res 2> make_template.err
EXECNOW: LOG list_files.res LOG list_files.err frama-c-script list-files %{dep:list_files.json} > list_files.res 2> list_files.err
EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 frama-c-script flamegraph %{dep:flamegraph.txt} . > flamegraph.res 2> flamegraph.err && rm -f flamegraph.svg
EXECNOW: LOG find_fun1.res LOG find_fun1.err frama-c-script find-fun main2 . > find_fun1.res 2> find_fun1.err
EXECNOW: LOG find_fun2.res LOG find_fun2.err frama-c-script find-fun main3 . > find_fun2.res 2> find_fun2.err
- EXECNOW: LOG find_fun3.res LOG find_fun3.err frama-c-script find-fun false_positive .> find_fun3.res 2> find_fun3.err
+ EXECNOW: LOG find_fun3.res LOG find_fun3.err frama-c-script find-fun false_positive . > find_fun3.res 2> find_fun3.err
*/
void main() {
diff --git a/tests/fc_script/oracle/list_files.res b/tests/fc_script/oracle/list_files.res
index 6ccc70819c87975dce26bc0351408d27cceb1c0a..f6c507d3db5f90b302f072eeb507d76a7d4dc7d3 100644
--- a/tests/fc_script/oracle/list_files.res
+++ b/tests/fc_script/oracle/list_files.res
@@ -1,30 +1,10 @@
# Paths as seen by a makefile inside subdirectory '.frama-c':
SRCS=\
-<<<<<<< HEAD
-main.c \
-main2.c \
-main3.c \
-||||||| 362083a770
-tests/fc_script/main.c \
-tests/fc_script/main2.c \
-tests/fc_script/main3.c \
-=======
-../tests/fc_script/main.c \
-../tests/fc_script/main2.c \
-../tests/fc_script/main3.c \
->>>>>>> origin/master
+../main.c \
+../main2.c \
+../main3.c \
-<<<<<<< HEAD
-# Possible definition of main function in the following file(s):
-main.c
-main3.c
-||||||| 362083a770
-# Possible definition of main function in the following file(s):
-tests/fc_script/main.c
-tests/fc_script/main3.c
-=======
# Possible definition of main function in the following file(s), as seen from '.frama-c':
-../tests/fc_script/main.c
-../tests/fc_script/main3.c
->>>>>>> origin/master
+../main.c
+../main3.c
diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i
index bb4e52f0410d0d08bd9a5cc0789e5626120a78c8..e089eba7b07b5f0bad066c7fe781075c097106ea 100644
--- a/tests/saveload/basic.i
+++ b/tests/saveload/basic.i
@@ -1,15 +1,15 @@
/* run.config
CMXS: @PTEST_NAME@
- EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./result/basic.sav > ./result/basic_sav.res 2> ./result/basic_sav.err
- EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva @EVA_OPTIONS@ -out -input -deps > ./result/basic_sav.1.res 2> ./result/basic_sav.1.err
- STDOPT: +"-load ./result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
+ EXECNOW: LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err BIN @PTEST_NAME@.sav (@frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -out -input -deps @PTEST_NAME@.i -save @PTEST_NAME@.sav) > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
+ EXECNOW: LOG @PTEST_NAME@_sav.1.res LOG @PTEST_NAME@_sav.1.err BIN @PTEST_NAME@.1.sav (@frama-c@ -save @PTEST_NAME@.1.sav @PTEST_NAME@.i -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 -journal-disable"
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
- STDOPT: +"-load ./result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print"
- STDOPT: +"-load ./result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
+ STDOPT: +"-load %{dep:@PTEST_NAME@.1.sav} -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print"
+ STDOPT: +"-load %{dep:@PTEST_NAME@.1.sav} -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
CMXS: status
- EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module status -save ./result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./result/status_sav.res 2> ./result/status_sav.err
- STDOPT: +"-load-module status -load ./result/status.sav"
- STDOPT: +"-load ./result/status.sav"
+ EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav (@frama-c@ -load-module status -save status.sav @PTEST_NAME@.i) > status_sav.res 2> status_sav.err
+ STDOPT: +"-load-module status.cmxs -load %{dep:status.sav}"
+ STDOPT: +"-load %{dep:status.sav}"
*/
int main() {
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index c79e10630fd9d80567c6184e2d4c606064678a04..ec0c20e2526dd3465ec5d25839cd17c853968d0d 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err ./bin/toplevel.opt -save ./result/bool.sav -eva @EVA_OPTIONS@ ./bool.c > result/bool_sav.res 2> result/bool_sav.err
- STDOPT: +"-load ./result/bool.sav -out -input -deps"
- STDOPT: +"-load ./result/bool.sav -eva @EVA_OPTIONS@"
+ EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err (@frama-c@ -save bool.sav -eva @EVA_OPTIONS@ ./bool.c) > bool_sav.res 2> bool_sav.err
+ STDOPT: +"-load %{dep:bool.sav} -out -input -deps"
+ STDOPT: +"-load %{dep:bool.sav} -eva @EVA_OPTIONS@"
*/
#include "stdbool.h"
diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i
index 8f63ff8bd4445ed03a4719b34ff365b1061dea0c..52a4623d0ff4cfcdc234b6104652d9c759b2b4b3 100644
--- a/tests/saveload/callbacks.i
+++ b/tests/saveload/callbacks.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav ./bin/toplevel.opt callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./result/callbacks.sav > ./result/callbacks_initial.res 2> ./result/callbacks_initial.err
- STDOPT: +"-load ./result/callbacks.sav -main main2 -then -main main3"
+ EXECNOW: LOG @PTEST_NAME@_initial.res LOG @PTEST_NAME@_initial.err BIN @PTEST_NAME@.sav (@frama-c@ @PTEST_NAME@.i -out -calldeps -eva-show-progress -main main1 -save @PTEST_NAME@.sav) > @PTEST_NAME@_initial.res 2> @PTEST_NAME@_initial.err
+ STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3"
*/
/* This tests whether the callbacks for callwise inout and from survive after
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index 5e95f55b41eed77400a2d9bd2ffeb8bc785954c7..df87623630029d882e46afab29e32fc10dbbc080 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,11 +1,11 @@
/* run.config
CMXS: deps_A deps_B deps_C deps_D deps_E
- EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module %{dep:deps_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./deps.i -save deps.sav > deps_sav.res 2> deps_sav.err
- STDOPT: +"-load-module %{dep:deps_A.cmxs} -load %{dep:deps.sav} -eva @EVA_OPTIONS@ -out -input -deps "
- STDOPT: +"-load-module %{dep:deps_B.cmxs} -load %{dep:deps.sav} -out -input -deps "
- STDOPT: +"-load-module %{dep:deps_C.cmxs} -load %{dep:deps.sav} -out -input -deps "
- STDOPT: +"-load-module %{dep:deps_D.cmxs} -load %{dep:deps.sav} -out -input -deps "
- STDOPT: +"-load-module %{dep:deps_E.cmxs} -load %{dep:deps.sav} -out -input -deps "
+ EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN @PTEST_NAME@.sav (@frama-c@ -load-module %{dep:deps_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps @PTEST_NAME@.i -save @PTEST_NAME@.sav) > deps_sav.res 2> deps_sav.err
+ STDOPT: +"-load-module %{dep:deps_A.cmxs} -load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps "
+ STDOPT: +"-load-module %{dep:deps_B.cmxs} -load %{dep:@PTEST_NAME@.sav} -out -input -deps "
+ STDOPT: +"-load-module %{dep:deps_C.cmxs} -load %{dep:@PTEST_NAME@.sav} -out -input -deps "
+ STDOPT: +"-load-module %{dep:deps_D.cmxs} -load %{dep:@PTEST_NAME@.sav} -out -input -deps "
+ STDOPT: +"-load-module %{dep:deps_E.cmxs} -load %{dep:@PTEST_NAME@.sav} -out -input -deps "
*/
int main() {
diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c
index f7f6f165f2c4e41b59b4c436e825ef56a3feaca9..119c23deec105aa9ad1d05b86cd3d7f0405b965e 100644
--- a/tests/saveload/isset.c
+++ b/tests/saveload/isset.c
@@ -1,9 +1,9 @@
/* run.config
- EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav ./bin/toplevel.opt -quiet -eva @EVA_OPTIONS@ -save result/isset.sav isset.c > ./result/isset_sav.res 2> ./result/isset_sav.err
- STDOPT: +"-quiet -load ./result/isset.sav"
- STDOPT: +"-load ./result/isset.sav"
- STDOPT: +"-eva @EVA_OPTIONS@ -load ./result/isset.sav"
- STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load ./result/isset.sav"
+ EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav (@frama-c@ -quiet -eva @EVA_OPTIONS@ -save isset.sav isset.c) > isset_sav.res 2> isset_sav.err
+ STDOPT: +"-quiet -load %{dep:isset.sav}"
+ STDOPT: +"-load %{dep:isset.sav}"
+ STDOPT: +"-eva @EVA_OPTIONS@ -load %{dep:isset.sav}"
+ STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load %{dep:isset.sav}"
*/
int main() {
diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i
index 081b3f6bb4f169be978f115fd6d57d98020799a0..8e7e3aa42433ffd2350e932010e59f772656d6b8 100644
--- a/tests/saveload/multi_project.i
+++ b/tests/saveload/multi_project.i
@@ -1,7 +1,7 @@
/* run.config
- EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > result/multi_project_sav.res 2> result/multi_project_sav.err
+ 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_NAME@.i) > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
CMXS: @PTEST_NAME@
- STDOPT: +"-load ./result/multi_project.sav -journal-disable"
+ STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -journal-disable"
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
OPT: -eva @EVA_OPTIONS@
*/
diff --git a/tests/saveload/oracle/basic.0.res.oracle b/tests/saveload/oracle/basic.0.res.oracle
index ae2056404eec150f128c3635e106f985a5b2b6bf..919ad3e4907c1f8e2bf010459d184911758aec0d 100644
--- a/tests/saveload/oracle/basic.0.res.oracle
+++ b/tests/saveload/oracle/basic.0.res.oracle
@@ -1,2 +1,2 @@
-[kernel] User Error: Frama-C state file 'result/basic.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/basic.1.res.oracle b/tests/saveload/oracle/basic.1.res.oracle
index f0e4f9fbeb86010035c9c1c0596e2db656c94818..2cf7ada66893ceb8fffd9b80ab2095c00320d0ee 100644
--- a/tests/saveload/oracle/basic.1.res.oracle
+++ b/tests/saveload/oracle/basic.1.res.oracle
@@ -1,2 +1,23 @@
-[kernel] User Error: Frama-C state file 'result/basic.1.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ int i;
+ int j;
+ i = 10;
+ /*@ assert i ≡ 10; */ ;
+ while (1) {
+ int tmp;
+ tmp = i;
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ i - 1; */
+ i --;
+ ;
+ if (! tmp) break;
+ }
+ j = 5;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/saveload/oracle/basic.2.res.oracle b/tests/saveload/oracle/basic.2.res.oracle
index f0e4f9fbeb86010035c9c1c0596e2db656c94818..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/basic.2.res.oracle
+++ b/tests/saveload/oracle/basic.2.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/basic.1.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/basic.4.res.oracle b/tests/saveload/oracle/basic.4.res.oracle
index 45d54e46c57d299d9994a7703be5c588e4980cd3..047acff3e8d77ced0f676b1de446cdbbe0c91952 100644
--- a/tests/saveload/oracle/basic.4.res.oracle
+++ b/tests/saveload/oracle/basic.4.res.oracle
@@ -1,2 +1,2 @@
-[kernel] User Error: Frama-C state file 'result/status.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index bc0690e630a04657a824d81c367565c69275bf4b..e25efee9d317c145520c4cdc931260d30ab51f1b 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -6,8 +6,7 @@
[eva] basic.i:19: assertion got status valid.
[eva] basic.i:20: starting to merge loop iterations
-[eva:alarm] basic.i:20: Warning:
- signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] basic.i:20: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index bc0690e630a04657a824d81c367565c69275bf4b..e25efee9d317c145520c4cdc931260d30ab51f1b 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -6,8 +6,7 @@
[eva] basic.i:19: assertion got status valid.
[eva] basic.i:20: starting to merge loop iterations
-[eva:alarm] basic.i:20: Warning:
- signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] basic.i:20: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/saveload/oracle/bool.0.res.oracle b/tests/saveload/oracle/bool.0.res.oracle
index 2dbdb27d5a52f6c4f4bce33fdffabb77209960af..f2e7096002831c02bbf21281a4c13821581bb843 100644
--- a/tests/saveload/oracle/bool.0.res.oracle
+++ b/tests/saveload/oracle/bool.0.res.oracle
@@ -1,2 +1,57 @@
-[kernel] User Error: Frama-C state file 'result/bool.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+[from] Computing for function f
+[from] Done for function f
+[from] Computing for function main
+[from] Computing for function printf_va_1 <-main
+[from] Done for function printf_va_1
+[from] Computing for function printf_va_2 <-main
+[from] Done for function printf_va_2
+[from] Computing for function printf_va_3 <-main
+[from] Done for function printf_va_3
+[from] Computing for function printf_va_4 <-main
+[from] Done for function printf_va_4
+[from] Computing for function printf_va_5 <-main
+[from] Done for function printf_va_5
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function f:
+ \result FROM \nothing
+[from] Function printf_va_1:
+ S___fc_stdout[0].__fc_FILE_data
+ FROM param0; S___fc_stdout[0]; "%d\n" (and SELF)
+ \result FROM param0; S___fc_stdout[0]; "%d\n"
+[from] Function printf_va_2:
+ S___fc_stdout[0].__fc_FILE_data
+ FROM param0; S___fc_stdout[0]; "%d\n" (and SELF)
+ \result FROM param0; S___fc_stdout[0]; "%d\n"
+[from] Function printf_va_3:
+ S___fc_stdout[0].__fc_FILE_data
+ FROM param0; param1; S___fc_stdout[0];
+ "%d,%d\n"[bits 0 to 55] (and SELF)
+ \result FROM param0; param1; S___fc_stdout[0]; "%d,%d\n"[bits 0 to 55]
+[from] Function printf_va_4:
+ S___fc_stdout[0].__fc_FILE_data
+ FROM param0; S___fc_stdout[0]; "%d\n" (and SELF)
+ \result FROM param0; S___fc_stdout[0]; "%d\n"
+[from] Function printf_va_5:
+ S___fc_stdout[0].__fc_FILE_data
+ FROM param0; S___fc_stdout[0]; "%d\n" (and SELF)
+ \result FROM param0; S___fc_stdout[0]; "%d\n"
+[from] Function main:
+ x FROM \nothing
+ y FROM \nothing
+ S___fc_stdout[0].__fc_FILE_data
+ FROM S___fc_stdout[0]; "%d\n"; "%d\n";
+ "%d,%d\n"[bits 0 to 55]; "%d\n"; "%d\n" (and SELF)
+ \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function f:
+ i; j; tmp; __retres
+[inout] Inputs for function f:
+ \nothing
+[inout] Out (internal) for function main:
+ x; y; S___fc_stdout[0].__fc_FILE_data
+[inout] Inputs for function main:
+ x; y; S___fc_stdout[0]; "%d\n"; "%d\n"; "%d,%d\n"[bits 0 to 55]; "%d\n";
+ "%d\n"
diff --git a/tests/saveload/oracle/bool.1.res.oracle b/tests/saveload/oracle/bool.1.res.oracle
index 2dbdb27d5a52f6c4f4bce33fdffabb77209960af..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/bool.1.res.oracle
+++ b/tests/saveload/oracle/bool.1.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/bool.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 2dccb86d209b08ee721881df6a9747a4e37e85c7..7a24197dd13a11b3d32faf881abf47700079f65b 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -9,39 +9,33 @@
Called from bool.c:25.
[eva] bool.c:17: assertion got status valid.
[eva] bool.c:18: starting to merge loop iterations
-[eva:alarm] bool.c:18: Warning:
- signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] bool.c:18: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function printf_va_1 <- main.
Called from bool.c:27.
[eva] using specification for function printf_va_1
-[eva] bool.c:27:
- function printf_va_1: precondition got status valid.
+[eva] bool.c:27: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function printf_va_2 <- main.
Called from bool.c:29.
[eva] using specification for function printf_va_2
-[eva] bool.c:29:
- function printf_va_2: precondition got status valid.
+[eva] bool.c:29: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
Called from bool.c:31.
[eva] using specification for function printf_va_3
-[eva] bool.c:31:
- function printf_va_3: precondition got status valid.
+[eva] bool.c:31: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function printf_va_4 <- main.
Called from bool.c:33.
[eva] using specification for function printf_va_4
-[eva] bool.c:33:
- function printf_va_4: precondition got status valid.
+[eva] bool.c:33: function printf_va_4: precondition got status valid.
[eva] Done for function printf_va_4
[eva] computing for function printf_va_5 <- main.
Called from bool.c:35.
[eva] using specification for function printf_va_5
-[eva] bool.c:35:
- function printf_va_5: precondition got status valid.
+[eva] bool.c:35: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/saveload/oracle/callbacks.res.oracle b/tests/saveload/oracle/callbacks.res.oracle
index ca875a6b02f316a5d3f996d09be20b4e749bea1f..ae9563d2b2b8ce582d84ca2bef1b6bd3dd9006f3 100644
--- a/tests/saveload/oracle/callbacks.res.oracle
+++ b/tests/saveload/oracle/callbacks.res.oracle
@@ -1,2 +1,111 @@
-[kernel] User Error: Frama-C state file 'result/callbacks.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+[eva] Analyzing a complete application starting at main2
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ x ∈ {0}
+ y ∈ {0}
+[eva] computing for function g1 <- main2.
+ Called from callbacks.i:30.
+[eva] computing for function f <- g1 <- main2.
+ Called from callbacks.i:16.
+[eva] Recording results for f
+[from] Computing for function f
+[from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g1
+[from] Computing for function g1
+[from] Done for function g1
+[eva] Done for function g1
+[eva] computing for function g2 <- main2.
+ Called from callbacks.i:31.
+[eva] computing for function f <- g2 <- main2.
+ Called from callbacks.i:21.
+[eva] Recording results for f
+[from] Computing for function f
+[from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g2
+[from] Computing for function g2
+[from] Done for function g2
+[eva] Done for function g2
+[eva] Recording results for main2
+[from] Computing for function main2
+[from] Done for function main2
+[eva] done for function main2
+[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
+[from] call to f at callbacks.i:16 (by g1):
+ x FROM p
+[from] call to f at callbacks.i:21 (by g2):
+ y FROM p
+[from] call to g1 at callbacks.i:30 (by main2):
+ x FROM \nothing
+[from] call to g2 at callbacks.i:31 (by main2):
+ y FROM \nothing
+[from] entry point:
+ x FROM \nothing
+ y FROM \nothing
+[from] ====== END OF CALLWISE DEPENDENCIES ======
+[inout] Out (internal) for function f:
+ x; y
+[inout] Out (internal) for function g1:
+ x
+[inout] Out (internal) for function g2:
+ y
+[inout] Out (internal) for function main2:
+ x; y
+[eva] Analyzing a complete application starting at main3
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ x ∈ {0}
+ y ∈ {0}
+[eva] computing for function g1 <- main3.
+ Called from callbacks.i:35.
+[eva] computing for function f <- g1 <- main3.
+ Called from callbacks.i:16.
+[eva] Recording results for f
+[from] Computing for function f
+[from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g1
+[from] Computing for function g1
+[from] Done for function g1
+[eva] Done for function g1
+[eva] computing for function g2 <- main3.
+ Called from callbacks.i:36.
+[eva] computing for function f <- g2 <- main3.
+ Called from callbacks.i:21.
+[eva] Recording results for f
+[from] Computing for function f
+[from] Done for function f
+[eva] Done for function f
+[eva] Recording results for g2
+[from] Computing for function g2
+[from] Done for function g2
+[eva] Done for function g2
+[eva] Recording results for main3
+[from] Computing for function main3
+[from] Done for function main3
+[eva] done for function main3
+[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
+[from] call to f at callbacks.i:16 (by g1):
+ x FROM p
+[from] call to f at callbacks.i:21 (by g2):
+ y FROM p
+[from] call to g1 at callbacks.i:35 (by main3):
+ x FROM \nothing
+[from] call to g2 at callbacks.i:36 (by main3):
+ y FROM \nothing
+[from] entry point:
+ x FROM \nothing
+ y FROM \nothing
+[from] ====== END OF CALLWISE DEPENDENCIES ======
+[inout] Out (internal) for function f:
+ x; y
+[inout] Out (internal) for function g1:
+ x
+[inout] Out (internal) for function g2:
+ y
+[inout] Out (internal) for function main3:
+ x; y
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 139c64b454f6e4eac7ee970596e5f2bce79e1c4b..4c959751d7cf4f524a5a61f5563fffb2481077c3 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -5,8 +5,7 @@
[eva:initial-state] Values of globals at initialization
[eva] deps.i:15: starting to merge loop iterations
-[eva:alarm] deps.i:15: Warning:
- signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] deps.i:15: Warning: signed overflow. assert -2147483648 ≤ i - 1;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/saveload/oracle/isset.0.res.oracle b/tests/saveload/oracle/isset.0.res.oracle
index be79b15a73bf2a3c7800c303a739e0fe84ee939e..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/isset.0.res.oracle
+++ b/tests/saveload/oracle/isset.0.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/isset.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.1.res.oracle b/tests/saveload/oracle/isset.1.res.oracle
index be79b15a73bf2a3c7800c303a739e0fe84ee939e..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/isset.1.res.oracle
+++ b/tests/saveload/oracle/isset.1.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/isset.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.2.res.oracle b/tests/saveload/oracle/isset.2.res.oracle
index be79b15a73bf2a3c7800c303a739e0fe84ee939e..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/isset.2.res.oracle
+++ b/tests/saveload/oracle/isset.2.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/isset.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset.3.res.oracle b/tests/saveload/oracle/isset.3.res.oracle
index be79b15a73bf2a3c7800c303a739e0fe84ee939e..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/isset.3.res.oracle
+++ b/tests/saveload/oracle/isset.3.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/isset.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/isset_sav.res b/tests/saveload/oracle/isset_sav.res
index e910722073c052e8ea08eb000b43f238b9fb8690..f2693a09a703f2ac60abde786ce875d8b5aaf428 100644
--- a/tests/saveload/oracle/isset_sav.res
+++ b/tests/saveload/oracle/isset_sav.res
@@ -1,2 +1 @@
-[eva:alarm] isset.c:13: Warning:
- signed overflow. assert -2147483648 ≤ i - 1;
+[eva:alarm] isset.c:13: Warning: signed overflow. assert -2147483648 ≤ i - 1;
diff --git a/tests/saveload/oracle/multi_project.0.res.oracle b/tests/saveload/oracle/multi_project.0.res.oracle
index 6039357f9a5415ef3ba7818875cab0e00ba4938d..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/multi_project.0.res.oracle
+++ b/tests/saveload/oracle/multi_project.0.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/multi_project.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/segfault_datatypes.res.oracle b/tests/saveload/oracle/segfault_datatypes.res.oracle
index 71193c073c31bad895cc25e346595b0b9579ec89..919ad3e4907c1f8e2bf010459d184911758aec0d 100644
--- a/tests/saveload/oracle/segfault_datatypes.res.oracle
+++ b/tests/saveload/oracle/segfault_datatypes.res.oracle
@@ -1,2 +1,2 @@
-[kernel] User Error: Frama-C state file 'result/segfault_datatypes.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/oracle/sparecode.res.oracle b/tests/saveload/oracle/sparecode.res.oracle
index 835c93783896d29c9cd32faef736d9470831c860..c1a75f49e233a3557ccc3efb28c191b714eaa1d5 100644
--- a/tests/saveload/oracle/sparecode.res.oracle
+++ b/tests/saveload/oracle/sparecode.res.oracle
@@ -1,2 +1 @@
-[kernel] User Error: Frama-C state file 'result/sparecode.sav' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i
index adf6f9ad9b0d932159ffb731a7a61553772e6eb5..a910d7d701d1a78320954db3f40fbed8c875ab9f 100644
--- a/tests/saveload/segfault_datatypes.i
+++ b/tests/saveload/segfault_datatypes.i
@@ -1,8 +1,8 @@
/* run.config
CMXS: segfault_datatypes_A segfault_datatypes_B
- EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module ./segfault_datatypes_A -eva @EVA_OPTIONS@ -out -input -deps ./segfault_datatypes.i -save ./result/segfault_datatypes.sav > ./result/segfault_datatypes_sav.res 2> ./result/segfault_datatypes_sav.err
- CMD: @frama-c@ -load-module ./segfault_datatypes_B
- STDOPT: +"-load ./result/segfault_datatypes.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
+ EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module %{dep:segfault_datatypes_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps %{dep:segfault_datatypes.i} -save segfault_datatypes.sav > segfault_datatypes_sav.res 2> segfault_datatypes_sav.err
+ CMD: @frama-c@ -load-module %{dep:segfault_datatypes_B.cmxs}
+ STDOPT: +"-load %{dep:segfault_datatypes.sav} -eva @EVA_OPTIONS@ -out -input -deps -journal-disable"
*/
diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i
index 3bc98d2b10009ddc789e0aeee46e932c6761d007..a54ccc4fffb743c5d75443c610580cc2bfa319b2 100644
--- a/tests/saveload/sparecode.i
+++ b/tests/saveload/sparecode.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err ./bin/toplevel.opt -slicing-level 2 -slice-return main -eva-show-progress -save ./result/sparecode.sav sparecode.i -then-on 'Slicing export' -print > result/sparecode_sav.res 2> result/sparecode_sav.err
- STDOPT: +"-load ./result/sparecode.sav"
+ EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err (@frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save sparecode.sav sparecode.i -then-on 'Slicing export' -print) > sparecode_sav.res 2> sparecode_sav.err
+ STDOPT: +"-load %{dep:sparecode.sav}"
*/
int G;