diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i index 4d9b50cd565baedf36d4ebb071a2915ff4527216..919f247cf5d6fb7f63b2b76707794dbf2b09428a 100644 --- a/tests/builtins/Longinit_sequencer.i +++ b/tests/builtins/Longinit_sequencer.i @@ -1,4 +1,4 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -res-file @PTEST_RESULT@ + EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@ */ diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i index d6e1f53181467a2ec7876261086d4a39869f7d19..84322912cb6c9b8a476d38e523f53629faab6d0a 100644 --- a/tests/builtins/big_local_array.i +++ b/tests/builtins/big_local_array.i @@ -1,8 +1,8 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs -OPT: -eva-show-progress -print -journal-disable -eva -report -OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report -OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva + EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs + OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report + OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report + OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva */ struct S { diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle index 6deb10c4aea0a67d5036bafc38745c7f19bd3406..2a0c3fd82a978552927c8aed7b96e5f48b92d07a 100644 --- a/tests/builtins/oracle/Longinit_sequencer.res.oracle +++ b/tests/builtins/oracle/Longinit_sequencer.res.oracle @@ -79,6 +79,8 @@ [eva] tests/builtins/long_init.c:77: Call to builtin free [eva] tests/builtins/long_init.c:77: function free: precondition 'freeable' got status valid. +[eva:malloc] tests/builtins/long_init.c:77: + strong free on bases: {__malloc_init_inner_l75} [eva] Recording results for init_inner [eva] Done for function init_inner [eva:locals-escaping] tests/builtins/long_init.c:85: Warning: @@ -161,6 +163,8 @@ [eva] tests/builtins/long_init.c:103: Call to builtin free [eva] tests/builtins/long_init.c:103: function free: precondition 'freeable' got status valid. +[eva:malloc] tests/builtins/long_init.c:103: + strong free on bases: {__malloc_init_inner_l73} [eva] tests/builtins/long_init.c:104: Call to builtin Frama_C_malloc_fresh for function malloc [eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104 @@ -435,6 +439,8 @@ Values at end of function main: [eva] tests/builtins/long_init2.c:103: Call to builtin free [eva] tests/builtins/long_init2.c:103: function free: precondition 'freeable' got status valid. +[eva:malloc] tests/builtins/long_init2.c:103: + strong free on bases: {__malloc_init_inner_l73} [eva] tests/builtins/long_init2.c:104: Call to builtin Frama_C_malloc_fresh for function malloc [eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104 @@ -670,6 +676,8 @@ Values at end of function main: [eva] tests/builtins/long_init3.c:103: Call to builtin free [eva] tests/builtins/long_init3.c:103: function free: precondition 'freeable' got status valid. +[eva:malloc] tests/builtins/long_init3.c:103: + strong free on bases: {__malloc_init_inner_l73} [eva] tests/builtins/long_init3.c:104: Call to builtin Frama_C_malloc_fresh for function malloc [eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104