diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index b8ac6adfa6d8d664e3dc23938619a1bca3348e7a..94fd7bc07f9a6d8c2388de74a98ea8db8cdc67c2 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -344,6 +344,7 @@ let example_msg =
@@frama-c@@ # Shortcut defined as follow: %s@ \
@@frama-c-cmd@@ # Shortcut defined as follow: %s@ \
@@frama-c-exe@@ # set to the value of the 'TOPLEVEL_PATH' variable from './tests/ptests_config' file.@ \
+ @@DEV_NULL@@ # set to 'NUL' for Windows platforms and to '/dev/null' otherwise.@ \
@]@ \
@[<v 1>\
Examples:@ \
@@ -776,6 +777,8 @@ let launch command_string =
s command_string;
exit 1
+let dev_null = if Sys.os_type = "Win32" then "NUL" else "/dev/null"
+
module Test_config: sig
val scan_directives: drop:bool ->
SubDir.t -> file:string -> Scanf.Scanning.in_channel -> config -> config
@@ -788,6 +791,7 @@ end = struct
"frama-c-exe", !toplevel_path;
"frama-c-cmd", !macro_frama_c_cmd;
"frama-c", !macro_frama_c;
+ "DEV_NULL", dev_null;
"PTEST_DEFAULT_OPTIONS", !macro_default_options;
"PTEST_OPTIONS", !macro_options;
"PTEST_PRE_OPTIONS", !macro_pre_options;
@@ -1687,10 +1691,11 @@ let do_filter =
(Filename.basename exec_name)
in
let unfiltered_file = Filename.sanitize (log_prefix ^ log_ext ^ ".unfiltered-log") in
- let filter_cmd = Format.sprintf "%s | %s%s > %s 2> /dev/null"
+ let filter_cmd = Format.sprintf "%s | %s%s > %s 2> %s"
(* the filter command can be a diff from a [@PTEST_ORACLE@] *)
(if Sys.file_exists unfiltered_file then "cat " ^ unfiltered_file else "echo \"\"")
exec_name params log_file
+ dev_null
in
if !verbosity >= 1
then lock_printf "%tFilter command:@\n%s@." print_default_env filter_cmd;
@@ -1712,8 +1717,8 @@ let compare_one_file cmp log_prefix oracle_prefix log_kind =
if not (Sys.file_exists oracle_file) then
check_file_is_empty_or_nonexisting (Command_error (cmp,log_kind)) ~log_file
else begin
- let cmp_string =
- !do_cmp ^ " " ^ log_file ^ " " ^ oracle_file ^ " > /dev/null 2> /dev/null"
+ let cmp_string = Format.sprintf "%s %s %s > %s 2> %s"
+ !do_cmp log_file oracle_file dev_null dev_null
in
if !verbosity >= 2 then lock_printf "%% cmp%s (%d) :%s@."
ext
@@ -1733,7 +1738,8 @@ let compare_one_log_file dir file =
end else
let log_file = Filename.sanitize (SubDir.make_result_file dir file) in
let oracle_file = Filename.sanitize (SubDir.make_oracle_file dir file) in
- let cmp_string = !do_cmp ^ " " ^ log_file ^ " " ^ oracle_file ^ " > /dev/null 2> /dev/null" in
+ let cmp_string = Format.sprintf "%s %s %s > %s 2> %s"
+ !do_cmp log_file oracle_file dev_null dev_null in
if !verbosity >= 2 then lock_printf "%% cmplog: %s / %s@." (SubDir.get dir) file;
ignore (launch_and_check_compare_file (Log_error (dir,file))
~cmp_string ~log_file ~oracle_file)
diff --git a/src/plugins/wp/diff_annot.0.execnow.txt b/src/plugins/wp/diff_annot.0.execnow.txt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/wp/tests/wp_region/annot.i b/src/plugins/wp/tests/wp_region/annot.i
index 23463af75a974c021bf5955e9689f873ac0c053e..93dd7b1cd7865ffb38467183c1273ba00ecb7b60 100644
--- a/src/plugins/wp/tests/wp_region/annot.i
+++ b/src/plugins/wp/tests/wp_region/annot.i
@@ -1,8 +1,11 @@
/* run.config
+ PLUGIN: wp
OPT: -region-annot -print
- EXECNOW: @frama-c@ -region-annot -print @PTEST_DIR@/@PTEST_NAME@.i -ocode @PTEST_DIR@/@PTEST_NAME@/a.i
- EXECNOW: @frama-c@ -region-annot -print @PTEST_DIR@/@PTEST_NAME@/a.i -ocode @PTEST_DIR@/@PTEST_NAME@/b.i > /dev/null
- EXECNOW: diff @PTEST_DIR@/@PTEST_NAME@/a.i @PTEST_DIR@/@PTEST_NAME@/b.i > /dev/null
+ EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ @PTEST_DIR@/@PTEST_NAME@.i -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
+ EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
+ EXECNOW: LOG diff_@PTEST_NAME@.txt diff @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
+COMMENT: The file diff_@PTEST_NAME@.txt must be empty.
+COMMENT: So, that file has not to be present into the oracle directory since absent files are considered such as empty files.
*/
/* run.config_qualif
diff --git a/src/plugins/wp/tests/wp_region/oracle/diff_annot.txt b/src/plugins/wp/tests/wp_region/oracle/diff_annot.txt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/compliance/check-json.i b/tests/compliance/check-json.i
index c59b0b2c74f7090f056a290caacb42bc506b2a26..1a3c99c12ae8d2d29779fb562ff4a14844816887 100644
--- a/tests/compliance/check-json.i
+++ b/tests/compliance/check-json.i
@@ -1,7 +1,7 @@
/*run.config
NOFRAMAC:
- EXECNOW: python3 -m json.tool < share/compliance/c11_functions.json >/dev/null
- EXECNOW: python3 -m json.tool < share/compliance/glibc_functions.json >/dev/null
- EXECNOW: python3 -m json.tool < share/compliance/nonstandard_identifiers.json >/dev/null
- EXECNOW: python3 -m json.tool < share/compliance/posix_identifiers.json >/dev/null
+ EXECNOW: LOG json_@PTEST_NAME@_1.txt python3 -m json.tool < share/compliance/c11_functions.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_1.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < share/compliance/glibc_functions.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_2.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_3.txt python3 -m json.tool < share/compliance/nonstandard_identifiers.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_3.txt 2> @DEV_NULL@
+ EXECNOW: LOG json_@PTEST_NAME@_4.txt python3 -m json.tool < share/compliance/posix_identifiers.json | head -n 2 > @PTEST_RESULT@/json_@PTEST_NAME@_4.txt 2> @DEV_NULL@
*/
diff --git a/tests/compliance/oracle/json_check-json_1.txt b/tests/compliance/oracle/json_check-json_1.txt
new file mode 100644
index 0000000000000000000000000000000000000000..1c7fc7039ae9a32a7e24b026fa194ade1cc32984
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_1.txt
@@ -0,0 +1,2 @@
+{
+ "description": "C11 reserved function identifiers",
diff --git a/tests/compliance/oracle/json_check-json_2.txt b/tests/compliance/oracle/json_check-json_2.txt
new file mode 100644
index 0000000000000000000000000000000000000000..a7490e8d444cf0359541826585e85c435704ea3e
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_2.txt
@@ -0,0 +1,2 @@
+{
+ "description": "Function and macro identifiers defined in the GNU C Library",
diff --git a/tests/compliance/oracle/json_check-json_3.txt b/tests/compliance/oracle/json_check-json_3.txt
new file mode 100644
index 0000000000000000000000000000000000000000..0b2f8f38fd6866c709dd788271b9c62fe2a52bf0
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_3.txt
@@ -0,0 +1,2 @@
+{
+ "description": "Non-ISO C, Non-POSIX identifiers known to the Frama-C standard library",
diff --git a/tests/compliance/oracle/json_check-json_4.txt b/tests/compliance/oracle/json_check-json_4.txt
new file mode 100644
index 0000000000000000000000000000000000000000..cdf3ccde431a21b0e3e97353e314452444a135a1
--- /dev/null
+++ b/tests/compliance/oracle/json_check-json_4.txt
@@ -0,0 +1,2 @@
+{
+ "description": "POSIX.1-2008 reserved function identifiers (plus a few legacy POSIX identifiers)",
diff --git a/tests/journal/control.i b/tests/journal/control.i
index a136fc4ec7a9ab6ed04a524260be23695e81cb7d..6a365c6c81a98cc996f01ef7b0a2117caf37cd7c 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,14 +1,14 @@
/* run.config
- COMMENT: do not compare generated journals since they depend on current time
- EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (./bin/toplevel.opt -journal-enable -check -eva -deps -out @EVA_OPTIONS@ -main f -journal-name tests/journal/result/control_journal.ml tests/journal/control.i && cp tests/journal/result/control_journal.ml tests/journal/result/control_journal_bis.ml) > /dev/null 2> /dev/null
- CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script tests/journal/result/control_journal -journal-disable
- CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script tests/journal/result/control_journal_bis -calldeps -journal-disable
- EXECNOW: make -s @PTEST_DIR@/abstract_cpt.cmxs
- EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null
- CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml
+ COMMENT: do not compare generated journals since they depend on current time
+ PLUGIN: @EVA_PLUGINS@
+ EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
+ OPT: -load-script control_journal.ml
+ MODULE:
+ EXECNOW: BIN control_journal_bis.ml cp control_journal.ml control_journal_bis.ml > @DEV_NULL@ 2> @DEV_NULL@
+ OPT: -calldeps -load-script control_journal_bis.ml
+ MODULE: abstract_cpt use_cpt
+ EXECNOW: BIN abstract_cpt_journal.ml @frama-c@ -journal-enable -journal-name abstract_cpt_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
+ OPT: -load-script abstract_cpt_journal.ml
*/
int x,y,c,d;
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 8e04f8022b2c5bddd51246e207e48be678a99c8f..0e3716b2ffb9aebe82488ec5eb7ab80b84850c8c 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,5 +1,5 @@
/* run.config
- EXECNOW: BIN control_journal2.ml ./bin/toplevel.opt -journal-enable -eva -deps -out -main f -journal-name tests/journal/result/control_journal2.ml tests/journal/control2.c > /dev/null 2> /dev/null
+ EXECNOW: BIN control_journal2.ml ./bin/toplevel.opt -journal-enable -eva -deps -out -main f -journal-name tests/journal/result/control_journal2.ml tests/journal/control2.c > @DEV_NULL@ 2> @DEV_NULL@
EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script tests/journal/result/control_journal2 -lib-entry -journal-name tests/journal/result/control_journal_next2.ml tests/journal/control2.c > ./tests/journal/result/control2_sav.res 2> ./tests/journal/result/control2_sav.err
CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
OPT: -load-script tests/journal/result/control_journal_next2
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 274b87c862bf5786beffcb180565eb82d3ddda93..62c76b4a3a1de55491fbb25daae2f125bf2f36c7 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,7 +1,7 @@
/* run.config
PLUGIN: @EVA_PLUGINS@ sparecode
MODULE: @PTEST_NAME@
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
+ EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > @DEV_NULL@ 2> @DEV_NULL@
CMD: @frama-c@
OPT: -load-script tests/journal/result/intra_journal -journal-disable
*/
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index bb282df999d8dca402c6ebdf6b5284021f50e629..22567e6e4de9558ddb133b356f041295fde4a0ca 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,6 @@
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o /dev/null
+ CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@
OPT:
*/