From fd0fdbc75614b23827f69ace3483f9d95b52c34b Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 15 Oct 2020 08:25:14 +0200
Subject: [PATCH] [Tests] tests/spec does not use @EVA_CONFIG@ by default
---
tests/spec/array_typedef.c | 4 ++--
tests/spec/assigns_result.i | 2 +-
tests/spec/assigns_void.c | 2 +-
tests/spec/behavior_assert.c | 6 +++---
tests/spec/default_assigns_bts0966.i | 2 +-
tests/spec/generalized_check.i | 2 +-
tests/spec/kw.c | 3 +++
tests/spec/logic_def.c | 2 +-
tests/spec/oracle/assigns_void.0.res.oracle | 2 +-
tests/spec/oracle/preprocess.res.oracle | 12 ++++++------
tests/spec/oracle/statement_behavior.res.oracle | 10 +++++-----
tests/spec/preprocess.c | 4 +++-
tests/spec/shifts.c | 2 +-
tests/spec/statement_behavior.c | 6 ++++--
tests/spec/test_config | 1 +
15 files changed, 34 insertions(+), 26 deletions(-)
diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 86387dcf427..a8273f59814 100644
--- a/tests/spec/array_typedef.c
+++ b/tests/spec/array_typedef.c
@@ -1,9 +1,9 @@
/*run.config
- OPT: -print -eva @EVA_CONFIG@ -journal-disable
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -print -eva @EVA_OPTIONS@ -journal-disable
*/
#define IP_FIELD 4
typedef int ip_address[IP_FIELD];
-
typedef struct {
ip_address src;
int dst[IP_FIELD];
diff --git a/tests/spec/assigns_result.i b/tests/spec/assigns_result.i
index f850166909e..bfde0dde8bf 100644
--- a/tests/spec/assigns_result.i
+++ b/tests/spec/assigns_result.i
@@ -1,8 +1,8 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-deps @EVA_OPTIONS@"
*/
int X,Y;
-
/*@ assigns \result;
assigns \exit_status;
*/
diff --git a/tests/spec/assigns_void.c b/tests/spec/assigns_void.c
index 6e70195b864..a93209867cb 100644
--- a/tests/spec/assigns_void.c
+++ b/tests/spec/assigns_void.c
@@ -1,10 +1,10 @@
/* run.config
OPT: -print -journal-disable -kernel-warn-key=annot-error=active
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -main g -print -no-annot -journal-disable
*/
//@ assigns *x;
void f(void *x);
-
void g() {
int y;
int* x = &y;
diff --git a/tests/spec/behavior_assert.c b/tests/spec/behavior_assert.c
index 2f5d7f97605..e130481efd9 100644
--- a/tests/spec/behavior_assert.c
+++ b/tests/spec/behavior_assert.c
@@ -1,8 +1,8 @@
/* run.config
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
-OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable -lib-entry
+ OPT: -eva @EVA_CONFIG@ -deps -out -input -journal-disable
*/
-
int e;
/*@
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index 6b4cd671eda..0bffe80560e 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -1,7 +1,7 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva -print
*/
-
int auto_states[4] ; // = { 1 , 0 , 0, 0 };
enum states {
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 5e604fd79a3..0068ae1099a 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
/* run.config
-PLUGIN: wp @PLUGIN@
+PLUGIN: wp @EVA_PLUGINS@
OPT: -wp -wp-prover qed -wp-msg-key shell
OPT: -eva -eva-use-spec f
OPT: -print
diff --git a/tests/spec/kw.c b/tests/spec/kw.c
index e57a4869f38..00a0fdd45a0 100644
--- a/tests/spec/kw.c
+++ b/tests/spec/kw.c
@@ -1,3 +1,6 @@
+/* run.config
+ PLUGIN: eva
+*/
typedef int assert;
assert behavior = 0;
diff --git a/tests/spec/logic_def.c b/tests/spec/logic_def.c
index a9050410d76..8448756e44a 100644
--- a/tests/spec/logic_def.c
+++ b/tests/spec/logic_def.c
@@ -1,7 +1,7 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
STDOPT: +"-eva -eva-verbose 2"
*/
-
//@ logic integer foo(int x) = x + 2 ;
int main() {
diff --git a/tests/spec/oracle/assigns_void.0.res.oracle b/tests/spec/oracle/assigns_void.0.res.oracle
index ef1300fb7fe..ee60596961b 100644
--- a/tests/spec/oracle/assigns_void.0.res.oracle
+++ b/tests/spec/oracle/assigns_void.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assigns_void.c (with preprocessing)
-[kernel:annot-error] assigns_void.c:5: Warning:
+[kernel:annot-error] assigns_void.c:6: Warning:
Cannot use a pointer to void here. Ignoring specification of function f
/* Generated by Frama-C */
void f(void *x);
diff --git a/tests/spec/oracle/preprocess.res.oracle b/tests/spec/oracle/preprocess.res.oracle
index 5fe944d4b41..8ef58928c2d 100644
--- a/tests/spec/oracle/preprocess.res.oracle
+++ b/tests/spec/oracle/preprocess.res.oracle
@@ -6,16 +6,16 @@
x ∈ {1}
y ∈ {1}
[eva] computing for function f <- main.
- Called from preprocess.c:24.
-[eva] preprocess.c:24: function f: precondition got status valid.
-[eva] preprocess.c:18:
+ Called from preprocess.c:26.
+[eva] preprocess.c:26: function f: precondition got status valid.
+[eva] preprocess.c:20:
function f, behavior default: postcondition got status valid.
[eva] Recording results for f
[eva] Done for function f
-[eva] preprocess.c:25: assertion got status valid.
-[eva] preprocess.c:28:
+[eva] preprocess.c:27: assertion got status valid.
+[eva] preprocess.c:30:
cannot evaluate ACSL term, unsupported ACSL construct: constant strings
-[eva:alarm] preprocess.c:28: Warning:
+[eva:alarm] preprocess.c:30: Warning:
assertion 'backslash_string' got status unknown.
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/spec/oracle/statement_behavior.res.oracle b/tests/spec/oracle/statement_behavior.res.oracle
index 225540226e3..4feb1f67ea2 100644
--- a/tests/spec/oracle/statement_behavior.res.oracle
+++ b/tests/spec/oracle/statement_behavior.res.oracle
@@ -5,13 +5,13 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function pfsqopfc <- main.
- Called from statement_behavior.c:23.
-[eva] statement_behavior.c:10: Warning:
+ Called from statement_behavior.c:25.
+[eva] statement_behavior.c:12: Warning:
no \from part for clause 'assigns five_times;'
-[eva:alarm] statement_behavior.c:17: Warning: assertion got status unknown.
-[eva:alarm] statement_behavior.c:4: Warning:
+[eva:alarm] statement_behavior.c:19: Warning: assertion got status unknown.
+[eva:alarm] statement_behavior.c:6: Warning:
function pfsqopfc: postcondition got status unknown.
-[eva:alarm] statement_behavior.c:18: Warning:
+[eva:alarm] statement_behavior.c:20: Warning:
accessing uninitialized left-value. assert \initialized(&five_times);
[eva] Recording results for pfsqopfc
[eva] Done for function pfsqopfc
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index bbe04e56572..f0fffe87941 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,7 +1,9 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
DEPS: preprocess.h
- OPT: -eva @EVA_CONFIG@ -journal-disable -print
+ OPT: -eva @EVA_OPTIONS@ -journal-disable -print
*/
+
// see bts 1357
#define assert(x) (x)?1:0
diff --git a/tests/spec/shifts.c b/tests/spec/shifts.c
index a7d934e68da..af132b55019 100644
--- a/tests/spec/shifts.c
+++ b/tests/spec/shifts.c
@@ -1,7 +1,7 @@
/* run.config
+ PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -deps -journal-disable
*/
-
int e;
/*@
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index e91bc047236..02551271d9e 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -1,11 +1,13 @@
/* run.config
- OPT: -eva @EVA_CONFIG@ -inout -journal-disable
+ PLUGIN: @EVA_PLUGINS@
+ OPT: -eva @EVA_OPTIONS@ -inout -journal-disable
*/
+
/*@ ensures \result == (int)(5 * x);
*/
int pfsqopfc(int x) {
-int five_times;
+int five_times;
/*@
assigns five_times;
ensures five_times == (int)(5 * x);
diff --git a/tests/spec/test_config b/tests/spec/test_config
index 55c0f5b0128..f43a4694237 100644
--- a/tests/spec/test_config
+++ b/tests/spec/test_config
@@ -2,4 +2,5 @@ COMMENT: for now, this directory mainly tests the annotations syntax,
COMMENT: no analysis is performed.
COMMENT: we continue on annotation errors, as this allows to put
COMMENT: various variations of the same test in one file.
+PLUGIN:
OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check
--
GitLab