From 25c9347852a7c118d7ca6a30da3f8a5958102ba3 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 30 Sep 2020 10:15:26 +0200
Subject: [PATCH] tests/syntax
---
Makefile | 5 ++++-
tests/syntax/Refresh_visitor.i | 4 ++--
tests/syntax/add_allocates.i | 4 ++--
tests/syntax/ast_init.i | 4 ++--
tests/syntax/char_is_unsigned.i | 4 ++--
tests/syntax/clone_test.i | 4 ++--
tests/syntax/enum_repr.i | 8 ++++----
tests/syntax/forloophook.i | 4 ++--
tests/syntax/get_astinfo_bts1136.i | 4 ++--
tests/syntax/ghost_parameters_formals_status.i | 4 ++--
tests/syntax/inserted_casts.c | 6 +++---
tests/syntax/logic_env.i | 4 ++--
tests/syntax/merge_loc.i | 4 ++--
tests/syntax/mutable_test.i | 4 ++--
tests/syntax/oracle/cpp-command.4.res.oracle | 2 +-
.../oracle/multiple_decls_contracts.0.res.oracle | 12 ++++++------
.../oracle/multiple_decls_contracts.1.res.oracle | 6 +++---
.../oracle/multiple_decls_contracts.2.res.oracle | 8 ++++----
tests/syntax/reorder.i | 4 ++--
tests/syntax/syntactic_hook.i | 4 ++--
tests/syntax/temporary_location.c | 4 ++--
tests/syntax/transient_block.i | 4 ++--
tests/syntax/typedef_multi_1.c | 4 ++--
tests/syntax/vdescr_bts1387.i | 5 +++--
tests/syntax/visit_create_local.i | 4 ++--
25 files changed, 62 insertions(+), 58 deletions(-)
diff --git a/Makefile b/Makefile
index fc65e9745d0..741e2385df6 100644
--- a/Makefile
+++ b/Makefile
@@ -166,7 +166,7 @@ force-reconfigure:
##############################################################################
-.PHONY: tests
+.PHONY: tests clean-tests
TESTS=cil float idct rte slicing scope value syntax misc builtins libc
tests: config.sed
@@ -174,6 +174,9 @@ tests: config.sed
dune exec -- ptests/ptests.exe
dune build $(addprefix @tests/,$(addsuffix /ptests,$(TESTS)))
+clean-tests:
+ rm -rf _build/default/tests
+
##############################################################################
.PHONY: install uninstall
diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i
index 8de4eb4bbb5..0c8262c9371 100644
--- a/tests/syntax/Refresh_visitor.i
+++ b/tests/syntax/Refresh_visitor.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -load-module %{dep:@PTEST_NAME@.cmxs} @EVA_OPTIONS@
+MODULE: @PTEST_NAME@.cmxs
+OPT: @EVA_OPTIONS@
*/
struct S { int i; };
diff --git a/tests/syntax/add_allocates.i b/tests/syntax/add_allocates.i
index 0dd2e067ee5..70657bf3c7f 100644
--- a/tests/syntax/add_allocates.i
+++ b/tests/syntax/add_allocates.i
@@ -1,9 +1,9 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print
+ MODULE: @PTEST_NAME@.cmxs
*/
+
int* x;
void f(void);
diff --git a/tests/syntax/ast_init.i b/tests/syntax/ast_init.i
index 090ec68974b..c596a3ccd01 100644
--- a/tests/syntax/ast_init.i
+++ b/tests/syntax/ast_init.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+MODULE: @PTEST_NAME@.cmxs
+OPT: -no-print
*/
int f(int x) { return x; }
diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i
index 0eb4739fe41..fe258c01c30 100644
--- a/tests/syntax/char_is_unsigned.i
+++ b/tests/syntax/char_is_unsigned.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: machdep_char_unsigned
- OPT:-print -load-module %{dep:machdep_char_unsigned.cmxs} -machdep unsigned_char -then -constfold -rte
+ MODULE: machdep_char_unsigned.cmxs
+ OPT:-print -machdep unsigned_char -then -constfold -rte
*/
char t[10];
diff --git a/tests/syntax/clone_test.i b/tests/syntax/clone_test.i
index f8d2bef0878..d712574d631 100644
--- a/tests/syntax/clone_test.i
+++ b/tests/syntax/clone_test.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+MODULE: @PTEST_NAME@.cmxs
+OPT: #"-no-print"
*/
/*@
diff --git a/tests/syntax/enum_repr.i b/tests/syntax/enum_repr.i
index 1ccb7935c91..b6497c51777 100644
--- a/tests/syntax/enum_repr.i
+++ b/tests/syntax/enum_repr.i
@@ -1,8 +1,8 @@
/* run.config
-CMXS: Enum_repr
-OPT: -load-module %{dep:Enum_repr.cmxs} -enums int -print
-OPT: -load-module %{dep:Enum_repr.cmxs} -enums gcc-short-enums -print
-OPT: -load-module %{dep:Enum_repr.cmxs} -enums gcc-enums -print
+MODULE: Enum_repr.cmxs
+OPT: -enums int -print
+OPT: -enums gcc-short-enums -print
+OPT: -enums gcc-enums -print
*/
// is represented by | int | gcc-enums | gcc-short-enums
diff --git a/tests/syntax/forloophook.i b/tests/syntax/forloophook.i
index 5d88397da3b..3d866b9e2a6 100644
--- a/tests/syntax/forloophook.i
+++ b/tests/syntax/forloophook.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+ MODULE: @PTEST_NAME@.cmxs
+ OPT: -no-autoload-plugins
*/
void f() {
for (int i=0; i< 10; i++);
diff --git a/tests/syntax/get_astinfo_bts1136.i b/tests/syntax/get_astinfo_bts1136.i
index 8d25ddc0bd0..28147c225aa 100644
--- a/tests/syntax/get_astinfo_bts1136.i
+++ b/tests/syntax/get_astinfo_bts1136.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+MODULE: @PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins
*/
int f (int x) { return x; }
int g (int x) { return x; }
diff --git a/tests/syntax/ghost_parameters_formals_status.i b/tests/syntax/ghost_parameters_formals_status.i
index ff6234d3d26..b51483928e8 100644
--- a/tests/syntax/ghost_parameters_formals_status.i
+++ b/tests/syntax/ghost_parameters_formals_status.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -load-module %{dep:@PTEST_NAME@.cmxs}
+ MODULE: @PTEST_NAME@.cmxs
+ OPT: -no-autoload-plugins
*/
void declaration_void(void) /*@ ghost (int x, int y) */ ;
diff --git a/tests/syntax/inserted_casts.c b/tests/syntax/inserted_casts.c
index fb708329abc..c8a2a0569b5 100644
--- a/tests/syntax/inserted_casts.c
+++ b/tests/syntax/inserted_casts.c
@@ -1,7 +1,7 @@
/* run.config
- CMXS: @PTEST_NAME@
- STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}"
- STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" +"-machdep x86_64"
+ MODULE: @PTEST_NAME@.cmxs
+ STDOPT: +"-no-autoload-plugins"
+ STDOPT: +"-no-autoload-plugins" +"-machdep x86_64"
*/
#include "stddef.h"
int f(int b)
diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i
index 112ec379971..090fb281c8f 100644
--- a/tests/syntax/logic_env.i
+++ b/tests/syntax/logic_env.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: logic_env_script
-OPT: -load-module %{dep:logic_env_script.cmxs}
+MODULE: logic_env_script.cmxs
+OPT: -no-autoload-plugins
*/
//@ predicate foo(integer x) = x == 0;
diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i
index bb5604134d8..11fae4b6422 100644
--- a/tests/syntax/merge_loc.i
+++ b/tests/syntax/merge_loc.i
@@ -1,8 +1,8 @@
/* run.config
- CMXS: pp_lines
- STDOPT: #"-load-module %{dep:pp_lines.cmxs}"
+ MODULE: pp_lines.cmxs
*/
+
// Test locations when cabs2cil merges declarations and tentative definitions
// together. We should always favor the tentative definition.
diff --git a/tests/syntax/mutable_test.i b/tests/syntax/mutable_test.i
index c14b31adc5a..fe4050f2774 100644
--- a/tests/syntax/mutable_test.i
+++ b/tests/syntax/mutable_test.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print
+MODULE: @PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -print
*/
struct R_1 {
diff --git a/tests/syntax/oracle/cpp-command.4.res.oracle b/tests/syntax/oracle/cpp-command.4.res.oracle
index 5cd16e50ce5..a85d472a341 100644
--- a/tests/syntax/oracle/cpp-command.4.res.oracle
+++ b/tests/syntax/oracle/cpp-command.4.res.oracle
@@ -1,2 +1,2 @@
[kernel] Preprocessing command:
- gcc -E -C -I LIBC -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 '/home/bobot/Sources/frama-c/_build/default/tests/syntax/result/cpp-command.c' -o '/tmp/FILE.i'
+ gcc -E -C -I LIBC -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 'FRAMA-C/tests/syntax/result/cpp-command.c' -o '/tmp/FILE.i'
diff --git a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
index b92cc616a72..9d50f76803e 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
@@ -4,12 +4,12 @@
[kernel] multiple_decls_contracts.c:11: Warning:
dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
/* Generated by Frama-C */
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_define_size_t.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_define_wchar_t.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_string_axiomatic.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h"
+#include "FRAMA-C/share/libc/__fc_define_size_t.h"
+#include "FRAMA-C/share/libc/__fc_define_wchar_t.h"
+#include "FRAMA-C/share/libc/__fc_string_axiomatic.h"
+#include "FRAMA-C/share/libc/string.h"
+#include "FRAMA-C/share/libc/strings.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
diff --git a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
index a42ae24841e..fdbaa0b6edc 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
@@ -4,9 +4,9 @@
[kernel] multiple_decls_contracts.c:11: Warning:
dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
/* Generated by Frama-C */
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h"
+#include "FRAMA-C/share/libc/string.h"
+#include "FRAMA-C/share/libc/strings.h"
#include "stddef.h"
#include "stdlib.h"
#include "string.h"
diff --git a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
index eba6fd7fe81..fa23074d9ee 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
@@ -4,10 +4,10 @@
[kernel] multiple_decls_contracts.c:11: Warning:
dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
/* Generated by Frama-C */
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_string_axiomatic.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
-#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "FRAMA-C/share/libc/__fc_alloc_axiomatic.h"
+#include "FRAMA-C/share/libc/__fc_string_axiomatic.h"
+#include "FRAMA-C/share/libc/string.h"
+#include "FRAMA-C/share/libc/strings.h"
#include "stddef.h"
#include "stdlib.h"
#include "string.h"
diff --git a/tests/syntax/reorder.i b/tests/syntax/reorder.i
index 647f6f9cea6..1199aeb932e 100644
--- a/tests/syntax/reorder.i
+++ b/tests/syntax/reorder.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+MODULE: @PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins
*/
int x;
diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i
index aabc12a7e61..f5a991909fd 100644
--- a/tests/syntax/syntactic_hook.i
+++ b/tests/syntax/syntactic_hook.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}"
+ MODULE: @PTEST_NAME@.cmxs
+ STDOPT: +"-no-autoload-plugins"
*/
int f(void);
diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c
index 11ce2caffb0..23e0d72c35b 100644
--- a/tests/syntax/temporary_location.c
+++ b/tests/syntax/temporary_location.c
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -print
+ MODULE: @PTEST_NAME@.cmxs
+ OPT: -print
*/
int f(void) {
diff --git a/tests/syntax/transient_block.i b/tests/syntax/transient_block.i
index 689cac47893..862cebdcc12 100644
--- a/tests/syntax/transient_block.i
+++ b/tests/syntax/transient_block.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -kernel-warn-key transient-block=active
+ MODULE: @PTEST_NAME@.cmxs
+ OPT: -kernel-warn-key transient-block=active
*/
void f(void) { }
diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c
index 09f9899655b..b8785672af9 100644
--- a/tests/syntax/typedef_multi_1.c
+++ b/tests/syntax/typedef_multi_1.c
@@ -1,7 +1,7 @@
/* run.config
DEPS: typedef_multi.h
- CMXS: typedef_multi
- OPT: -load-module %{dep:typedef_multi.cmxs} %{dep:typedef_multi_2.c}
+ MODULE: typedef_multi.cmxs
+ OPT: %{dep:typedef_multi_2.c}
*/
#include "typedef_multi.h"
diff --git a/tests/syntax/vdescr_bts1387.i b/tests/syntax/vdescr_bts1387.i
index 9ad26b98011..788665f995c 100644
--- a/tests/syntax/vdescr_bts1387.i
+++ b/tests/syntax/vdescr_bts1387.i
@@ -1,7 +1,8 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}
+MODULE: @PTEST_NAME@.cmxs
+OPT: #"-no-print"
*/
+
int f(int);
int g(int);
diff --git a/tests/syntax/visit_create_local.i b/tests/syntax/visit_create_local.i
index 21caf17f854..178b62c4318 100644
--- a/tests/syntax/visit_create_local.i
+++ b/tests/syntax/visit_create_local.i
@@ -1,5 +1,5 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -then-on bidon -print
+MODULE: @PTEST_NAME@.cmxs
+OPT: -then-on bidon -print
*/
void main() { int x,y; x = y; }
--
GitLab