From f3235ab8febe757ad5ba0c37a97f379c59812a2b Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 29 Sep 2020 14:33:48 +0200
Subject: [PATCH] adds deps to some tests
---
tests/cil/cpu_a.c | 2 +-
tests/cil/merge.c | 2 +-
tests/cil/merge2.c | 2 +-
tests/idct/ieee_1180_1990.c | 2 +-
tests/spec/first.c | 2 +-
tests/spec/merge_logic_globals_1.c | 3 ++-
tests/spec/model1.c | 4 ++--
tests/spec/multiple_decl_def_1.c | 2 +-
tests/spec/multiple_file_1.c | 2 +-
tests/spec/multiple_include_2.c | 4 ++--
tests/spec/preprocess.c | 2 +-
tests/spec/source_annot.c | 1 +
tests/spec/use.c | 3 ++-
tests/spec/volatile.c | 4 ++--
14 files changed, 19 insertions(+), 16 deletions(-)
diff --git a/tests/cil/cpu_a.c b/tests/cil/cpu_a.c
index cdcf2b854df..ceca6e498ad 100644
--- a/tests/cil/cpu_a.c
+++ b/tests/cil/cpu_a.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: cpu_b.c -machdep x86_16 -print
+ OPT: %{dep:cpu_b.c} -machdep x86_16 -print
*/
typedef unsigned short DWORD ;
diff --git a/tests/cil/merge.c b/tests/cil/merge.c
index 6c20a48a3a7..e8df7eb815b 100644
--- a/tests/cil/merge.c
+++ b/tests/cil/merge.c
@@ -1,4 +1,4 @@
/* run.config
- OPT: merge2.c -print
+ OPT: %{dep:merge2.c} -print
*/
int x;
diff --git a/tests/cil/merge2.c b/tests/cil/merge2.c
index fa57eb5c8c0..3fde680c426 100644
--- a/tests/cil/merge2.c
+++ b/tests/cil/merge2.c
@@ -1,4 +1,4 @@
/* run.config
- OPT: merge.c -print
+ OPT: %{dep:merge.c} -print
*/
int x =2;
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index e4690c3aa39..724ddbbe03a 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -1,6 +1,6 @@
/* run.config*
GCC:
- STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
+ STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow %{dep:idct.c} -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
*/
/* IEEE_1180_1990: a testbed for IDCT accuracy
* Copyright (C) 2001 Renaud Pacalet
diff --git a/tests/spec/first.c b/tests/spec/first.c
index 1aa3f9c6084..cb2b53247eb 100644
--- a/tests/spec/first.c
+++ b/tests/spec/first.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -print third.c second.c -journal-disable
+ OPT: -print %{dep:third.c} %{dep:second.c} -journal-disable
*/
/*@ behavior b:
requires \valid(first);
diff --git a/tests/spec/merge_logic_globals_1.c b/tests/spec/merge_logic_globals_1.c
index a8da2031733..ff35654fd72 100644
--- a/tests/spec/merge_logic_globals_1.c
+++ b/tests/spec/merge_logic_globals_1.c
@@ -1,5 +1,6 @@
/* run.config
-OPT: -print @PTEST_DIR@/merge_logic_globals_2.c -cpp-extra-args="-I@PTEST_DIR@"
+DEPS: merge_logic_globals.h
+OPT: -print %{dep:merge_logic_globals_2.c} -cpp-extra-args="-I@PTEST_DIR@"
*/
#include "merge_logic_globals.h"
diff --git a/tests/spec/model1.c b/tests/spec/model1.c
index 054e75ebadc..9dc7cfbdabe 100644
--- a/tests/spec/model1.c
+++ b/tests/spec/model1.c
@@ -1,7 +1,7 @@
/* run.config
-STDOPT: +"model2.c"
+DEPS: model1.h
+STDOPT: +"%{dep:model2.c}"
*/
-
#include "model1.h"
void main () {
diff --git a/tests/spec/multiple_decl_def_1.c b/tests/spec/multiple_decl_def_1.c
index 3deb71b988c..3ca910a501e 100644
--- a/tests/spec/multiple_decl_def_1.c
+++ b/tests/spec/multiple_decl_def_1.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -print multiple_decl_def_2.c -journal-disable
+ OPT: -print %{dep:multiple_decl_def_2.c} -journal-disable
*/
/* see bug #43 && #128 */
diff --git a/tests/spec/multiple_file_1.c b/tests/spec/multiple_file_1.c
index 82bc735d326..0f4879e8a5e 100644
--- a/tests/spec/multiple_file_1.c
+++ b/tests/spec/multiple_file_1.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -print multiple_file_2.c -journal-disable
+ OPT: -print %{dep:multiple_file_2.c} -journal-disable
*/
/* see bug #43 */
diff --git a/tests/spec/multiple_include_2.c b/tests/spec/multiple_include_2.c
index bf0d286ea07..df671ee8502 100644
--- a/tests/spec/multiple_include_2.c
+++ b/tests/spec/multiple_include_2.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: -kernel-warn-key=annot-error=active -print multiple_include_1.c -journal-disable
+ DEPS: multiple_include.h
+ OPT: -kernel-warn-key=annot-error=active -print %{dep:multiple_include_1.c} -journal-disable
*/
#include "multiple_include.h"
-
/*@ requires p(x); */
void bar(int x) { i+=x; return; }
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index 64b0e62aeec..bbe04e56572 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,7 +1,7 @@
/* run.config
+ DEPS: preprocess.h
OPT: -eva @EVA_CONFIG@ -journal-disable -print
*/
-
// see bts 1357
#define assert(x) (x)?1:0
diff --git a/tests/spec/source_annot.c b/tests/spec/source_annot.c
index ad85f6c8dc7..edcff9c183d 100644
--- a/tests/spec/source_annot.c
+++ b/tests/spec/source_annot.c
@@ -1,4 +1,5 @@
/* run.config
+ DEPS: prec_i.h
DONTRUN: static local variables & specifications
*/
typedef int INTEGER;
diff --git a/tests/spec/use.c b/tests/spec/use.c
index 327496a599e..ed96fb0f9bc 100644
--- a/tests/spec/use.c
+++ b/tests/spec/use.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: +"use2.c"
+ DEPS: dec.h
+ STDOPT: +"%{dep:use2.c}"
*/
// BTS 0887
diff --git a/tests/spec/volatile.c b/tests/spec/volatile.c
index 25dc52728ef..6a077533680 100644
--- a/tests/spec/volatile.c
+++ b/tests/spec/volatile.c
@@ -1,7 +1,7 @@
/* run.config
- OPT: volatile_aux.c -print -copy
+ DEPS: volatile.h
+ OPT: %{dep:volatile_aux.c} -print -copy
*/
-
#include "volatile.h"
//@volatile x,y writes w ;
--
GitLab