diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i index 1f733301b5c7942857df1515ef02528852f4a8bf..d69c1a3b38c537d6b2ea6bd2714c3a3f3f0c03cd 100644 --- a/tests/saveload/basic.i +++ b/tests/saveload/basic.i @@ -3,12 +3,11 @@ EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" - CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print" + STDOPT: #"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print" STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" EXECNOW: make -s @PTEST_DIR@/status.cmxs EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err - STDOPT: +"-load-module @PTEST_DIR@/status -load ./tests/saveload/result/status.sav" + STDOPT: #"-load-module @PTEST_DIR@/status" +"-load ./tests/saveload/result/status.sav" STDOPT: +"-load ./tests/saveload/result/status.sav" */ diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res index 056059606204259f47c4619d6aa71f6dd14adaa0..985eb96467566d2d7978358d57e350538de45307 100644 --- a/tests/saveload/oracle/basic_sav.1.res +++ b/tests/saveload/oracle/basic_sav.1.res @@ -4,9 +4,9 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/saveload/basic.i:19: assertion got status valid. -[eva] tests/saveload/basic.i:20: starting to merge loop iterations -[eva:alarm] tests/saveload/basic.i:20: Warning: +[eva] tests/saveload/basic.i:18: assertion got status valid. +[eva] tests/saveload/basic.i:19: starting to merge loop iterations +[eva:alarm] tests/saveload/basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1; [eva] Recording results for main [eva] done for function main diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res index 056059606204259f47c4619d6aa71f6dd14adaa0..985eb96467566d2d7978358d57e350538de45307 100644 --- a/tests/saveload/oracle/basic_sav.res +++ b/tests/saveload/oracle/basic_sav.res @@ -4,9 +4,9 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/saveload/basic.i:19: assertion got status valid. -[eva] tests/saveload/basic.i:20: starting to merge loop iterations -[eva:alarm] tests/saveload/basic.i:20: Warning: +[eva] tests/saveload/basic.i:18: assertion got status valid. +[eva] tests/saveload/basic.i:19: starting to merge loop iterations +[eva:alarm] tests/saveload/basic.i:19: Warning: signed overflow. assert -2147483648 ≤ i - 1; [eva] Recording results for main [eva] done for function main diff --git a/tests/saveload/oracle/segfault_datatypes_sav.res b/tests/saveload/oracle/segfault_datatypes_sav.res index a67d19e53c35d8b2b99e4d14186c88dd929a4f51..d84d5a9b2f1fd82a92b726a423231a894f1247e5 100644 --- a/tests/saveload/oracle/segfault_datatypes_sav.res +++ b/tests/saveload/oracle/segfault_datatypes_sav.res @@ -4,8 +4,8 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/saveload/segfault_datatypes.i:13: starting to merge loop iterations -[eva:alarm] tests/saveload/segfault_datatypes.i:13: Warning: +[eva] tests/saveload/segfault_datatypes.i:12: starting to merge loop iterations +[eva:alarm] tests/saveload/segfault_datatypes.i:12: Warning: signed overflow. assert -2147483648 ≤ i - 1; [eva] Recording results for main [eva] done for function main diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i index 7d6c97c42832cdb0edb6beadd038443b9e925186..021df2f49372ecd4d9633a5c9dc94a9f945fa341 100644 --- a/tests/saveload/segfault_datatypes.i +++ b/tests/saveload/segfault_datatypes.i @@ -1,8 +1,7 @@ -/* run.config +/* run.config* EXECNOW: make -s ./tests/saveload/segfault_datatypes_A.cmxs ./tests/saveload/segfault_datatypes_B.cmxs EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -load-module ./tests/saveload/segfault_datatypes_A -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/segfault_datatypes.i -save ./tests/saveload/result/segfault_datatypes.sav > ./tests/saveload/result/segfault_datatypes_sav.res 2> ./tests/saveload/result/segfault_datatypes_sav.err - CMD: @frama-c@ -load-module ./tests/saveload/segfault_datatypes_B - STDOPT: +"-load ./tests/saveload/result/segfault_datatypes.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" + STDOPT: +"-load-module ./tests/saveload/segfault_datatypes_B -load ./tests/saveload/result/segfault_datatypes.sav -eva -out -input -deps -journal-disable" */