diff --git a/Makefile b/Makefile index fc65e9745d09fa2ea349358cf6f9547d65eba59f..741e2385df69ab108a1b7ed64c3891b209f05d02 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 8de4eb4bbb52576308294f07bcf435cc9515155a..0c8262c9371ce859bb21ad8e629588d98201c4ec 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 0dd2e067ee54ac2e3b6fdbe38f63076ab054523a..70657bf3c7feb7ba85203b1382e459f0320863b7 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 090ec68974b926fb688a7cdf1d3172a364f19b90..c596a3ccd01ddbab7e48f04076552cb41201e9ad 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 0eb4739fe4188dc696ddd1033907db926be30e0c..fe258c01c30d2480743b02200c20bbfade137437 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 f8d2bef0878f37d74705840baab0d2f0a724ef1b..d712574d6316027428ef7e4031cfeb07c4e248c0 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 1ccb7935c91e1b5bc237329a2b8a7381ebd9c3ac..b6497c51777af496a5b7dceafa902b536340f1bc 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 5d88397da3bfb9dd32972441303c521d33757bdf..3d866b9e2a63ea6622cf1d0428493ccd53998781 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 8d25ddc0bd0d12c2f9d020d4d2923e10d7320af9..28147c225aaf5b4dfb3127343be0d488b4a8feb2 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 ff6234d3d265558943219bb32810c07df6cc2f92..b51483928e80431eac5c9063b6e0c23e7c044389 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 fb708329abc0d007b7099675c41af17d341f937d..c8a2a0569b5507e9a29d3bd618bc0483c5e1801b 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 112ec37997119c177cebc829690d935decf1670c..090fb281c8f283b69da20f52530bda4c9929f430 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 bb5604134d82f05ee4a5c3555ee8f35ecb6868f4..11fae4b642290299201c2ce5a20fe9f99019a88d 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 c14b31adc5a0643589b27643c5fb6845d4522b35..fe4050f277414eec61bfe8ec964dc220436e9c02 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 5cd16e50ce522b8af4b2e27df59253891ce9a5dd..a85d472a341bae0007a9dee2eea0d46daf63501d 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 b92cc616a72d44e34d58def745647a8262b8bed2..9d50f76803e83700d56c593b7284ec8f4387a977 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 a42ae24841efb503a4311f1a874ca869a40bb42f..fdbaa0b6edca8027b612043785280b94a0c3c4bc 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 eba6fd7fe81777f36afe9b8ee279a6702bdea3e0..fa23074d9ee2e35aa9deeb7a7697af756bb1cba6 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 647f6f9cea62343e958d96e170317cf1801f2bd8..1199aeb932e9cde121b928195e24a84f3eab793f 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 aabc12a7e6141304817d70705c2eeeb7b07acaf6..f5a991909fd664170edabb49416ad2550e62228c 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 11ce2caffb0c5cb2dccb453a454498f343b718c3..23e0d72c35b704c165249aa91b629db7e754d19d 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 689cac478935ff34888aae67cbeab49780377a19..862cebdcc12e3653a7f3534a536a1cec08d99a3d 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 09f9899655b5e12f834d896dc2215120ecd71904..b8785672af9c5eef9dea5373d06ed98b3e37155e 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 9ad26b98011cde070ec318ec65fccef660fe0f5a..788665f995cc75006d84c0e3eefecf01ad3af5fd 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 21caf17f85477ed351eb0715ad637c04d102528b..178b62c4318aed958a6efb31d76981f3021211ad 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; }