From 160c5c500b914852487004e26075a90c27c607e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Apr 2019 10:37:49 +0200
Subject: [PATCH] [tests] Uses the EVA_OPTIONS macro in the builtins tests.
---
tests/builtins/Longinit_sequencer.i | 4 ++--
tests/builtins/big_local_array.i | 8 ++++----
tests/builtins/oracle/Longinit_sequencer.res.oracle | 8 ++++++++
3 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i
index 4d9b50cd565..919f247cf5d 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 d6e1f531814..84322912cb6 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 6deb10c4aea..2a0c3fd82a9 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
--
GitLab