Skip to content
Snippets Groups Projects
Commit 160c5c50 authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[tests] Uses the EVA_OPTIONS macro in the builtins tests.

parent 88bf3236
No related branches found
No related tags found
No related merge requests found
/* run.config* /* run.config*
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -res-file @PTEST_RESULT@ OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@
*/ */
/* run.config* /* run.config*
EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
OPT: -eva-show-progress -print -journal-disable -eva -report OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report OPT: @EVA_OPTIONS@ -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 OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva
*/ */
struct S { struct S {
......
...@@ -79,6 +79,8 @@ ...@@ -79,6 +79,8 @@
[eva] tests/builtins/long_init.c:77: Call to builtin free [eva] tests/builtins/long_init.c:77: Call to builtin free
[eva] tests/builtins/long_init.c:77: [eva] tests/builtins/long_init.c:77:
function free: precondition 'freeable' got status valid. 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] Recording results for init_inner
[eva] Done for function init_inner [eva] Done for function init_inner
[eva:locals-escaping] tests/builtins/long_init.c:85: Warning: [eva:locals-escaping] tests/builtins/long_init.c:85: Warning:
...@@ -161,6 +163,8 @@ ...@@ -161,6 +163,8 @@
[eva] tests/builtins/long_init.c:103: Call to builtin free [eva] tests/builtins/long_init.c:103: Call to builtin free
[eva] tests/builtins/long_init.c:103: [eva] tests/builtins/long_init.c:103:
function free: precondition 'freeable' got status valid. 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: [eva] tests/builtins/long_init.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104 [eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
...@@ -435,6 +439,8 @@ Values at end of function main: ...@@ -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: Call to builtin free
[eva] tests/builtins/long_init2.c:103: [eva] tests/builtins/long_init2.c:103:
function free: precondition 'freeable' got status valid. 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: [eva] tests/builtins/long_init2.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104 [eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
...@@ -670,6 +676,8 @@ Values at end of function main: ...@@ -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: Call to builtin free
[eva] tests/builtins/long_init3.c:103: [eva] tests/builtins/long_init3.c:103:
function free: precondition 'freeable' got status valid. 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: [eva] tests/builtins/long_init3.c:104:
Call to builtin Frama_C_malloc_fresh for function malloc Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104 [eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104
......
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