diff --git a/tests/spec/array_typedef.c b/tests/spec/array_typedef.c
index 86387dcf4273550cd3a88f637d544008c16bacdb..a8273f598146e1ddb45647df4ec7477d47f347f9 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 f850166909efe129536bc4b54cae90447f6dbaaa..bfde0dde8bfeafeac8e63a972479dfcc80b2e97e 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 6e70195b864bfe5bb5f5d6f5c48ae74d798d9fbf..a93209867cbbc10b8f6a74157690640881a02ca9 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 2f5d7f9760516f5bb73dea22b220b91f2e07edc3..e130481efd9d88ce982877e44d3abc01814783a3 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 6b4cd671eda66ecb86c8a548620127b06604a1e6..0bffe80560eef462f8bf954d9093a8b8d854ed30 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 5e604fd79a3e8928733876af7ac76f7645fbd722..0068ae1099a05428a94a14047f15735fcb219756 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 e57a4869f38f02d6bb9c79f6e7c7b1b7139b50fc..00a0fdd45a0ec2bacea100137b0ea90342e4f1da 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 a9050410d76999cd48d4168575d26b22c5760e8d..8448756e44a5693e646a07608132edc247187e26 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 ef1300fb7fe89a4f7228f89384988ccf56b69afe..ee60596961bfab0414473522ebbab81d1049761c 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 5fe944d4b4146f90bb3b409d625e983227315e18..8ef58928c2dc6894452b4d22930c42633c4a4f5d 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 225540226e3a237d0208cc020eb78db127076b94..4feb1f67ea2b49809f46183a73e81ea64b41223b 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 bbe04e56572f5d979c00b1cb85766b0db75b5f79..f0fffe879411fdcf440017be7e49ce147f2076af 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 a7d934e68da3bb28a16e8b0922eb34cc823694dc..af132b55019639d055ded6f3464464409f32d442 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 e91bc04723652701f7477a479ac8abf29fbacac5..02551271d9e7eb7da938ec7026e539693397beb3 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 55c0f5b0128562d71d83efd28ff2c3d025a3fc25..f43a4694237743d39446812134ab8f4c79856562 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