diff --git a/README.md b/README.md
index 4c47961f33f64c3c0fe8bb3859b2787d9f315036..8578ceb2cd425f51d6d00493a5b14ee3e8a6f1b1 100644
--- a/README.md
+++ b/README.md
@@ -155,19 +155,30 @@ apt install xsltproc
Then launch tests:
```
-dune build @tests/regression_tests/runtest --no-buffer
+dune runtest tests/regression_tests --no-buffer
```
### ACSL verification tests
+To launch verification tests, create a directory `<my_dir>/` in
+`lustrec_tests/`. The directory must contain symbolic links to
+`lustrec_tests/{test.ml,dune}` and to relevant Lustre files in
+`lustrec_tests/lustre_files`, and a JSON configuration file `config.json`. See
+`lustrec_tests/{stopwatch_test,minimal_tests,offline_tests}` for example setups.
+The fields of the configuration file are all optional (default values are
+provided).
+
+To launch the tests:
```
-dune build @offline_tests/runtest --no-buffer
+dune runtest lustrec_tests/<my_dir> --no-buffer --display quiet
```
+The results can be found in the `results/` directory.
+
## Developing and hacking LustreC
If you want to hack LustreC, you should use
-[dune](https://dune.readthedocs.io/en/latest/ "Link to dune
-documentation") to build and execute it.
+[dune](https://dune.readthedocs.io/en/latest/ "Link to dune documentation") to
+build and execute it.
To build LustreC with dune:
diff --git a/lustrec_tests/dune b/lustrec_tests/dune
new file mode 100644
index 0000000000000000000000000000000000000000..5b79b1cab38b05c941c63b6a707565c7e8953281
--- /dev/null
+++ b/lustrec_tests/dune
@@ -0,0 +1,13 @@
+(env
+ (dev
+ (flags (:standard -w -32))))
+
+(test
+ (name test)
+ (libraries re unix yojson)
+ (deps
+ (:lus (glob_files *.lus))
+ (:cfg config.json)
+ (glob_files *)) ; to include `ignored` if its present
+ (action
+ (run %{test} %{project_root} %{bin:lustrec} %{cfg} "%{lus}")))
diff --git a/lustrec_tests/minimal_tests_O1/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/Abs1_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Abs1_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Abs1_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests/Assignment1.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Assignment1.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Assignment1.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/BitwiseXOR_int8_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/BitwiseXOR_int8_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/BitwiseXOR_int8_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/Clock_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Clock_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Clock_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/ForEach1_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/ForEach1_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/ForEach1_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/LookupTable1D_2points_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/LookupTable1D_2points_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/LookupTable1D_2points_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests/Product1.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/Product1.LUSTREC.lus
rename to lustrec_tests/minimal_tests/Product1.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/SYNAPSE_1.lus b/lustrec_tests/minimal_tests/SYNAPSE_1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/SYNAPSE_1.lus
rename to lustrec_tests/minimal_tests/SYNAPSE_1.lus
diff --git a/lustrec_tests/minimal_tests_O1/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests/UnitDelay_PP.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/UnitDelay_PP.LUSTREC.lus
rename to lustrec_tests/minimal_tests/UnitDelay_PP.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/_6counter.lus b/lustrec_tests/minimal_tests/_6counter.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/_6counter.lus
rename to lustrec_tests/minimal_tests/_6counter.lus
diff --git a/lustrec_tests/minimal_tests_O1/clocks1.lus b/lustrec_tests/minimal_tests/clocks1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/clocks1.lus
rename to lustrec_tests/minimal_tests/clocks1.lus
diff --git a/lustrec_tests/minimal_tests/config.json b/lustrec_tests/minimal_tests/config.json
new file mode 100644
index 0000000000000000000000000000000000000000..75d2d8eadea04966a69bcc06d78cb74255c12ea7
--- /dev/null
+++ b/lustrec_tests/minimal_tests/config.json
@@ -0,0 +1,5 @@
+{
+ "initial_timeout": 240,
+ "optimization_level": 1,
+ "ignored_file": null
+}
diff --git a/lustrec_tests/minimal_tests/dune b/lustrec_tests/minimal_tests/dune
new file mode 120000
index 0000000000000000000000000000000000000000..55afef878ff2c0566e6fd92d804c17520ccc9a12
--- /dev/null
+++ b/lustrec_tests/minimal_tests/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O1/hysteresis_1.lus b/lustrec_tests/minimal_tests/hysteresis_1.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/hysteresis_1.lus
rename to lustrec_tests/minimal_tests/hysteresis_1.lus
diff --git a/lustrec_tests/minimal_tests_O1/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests/inv_M_2x2.LUSTREC.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/inv_M_2x2.LUSTREC.lus
rename to lustrec_tests/minimal_tests/inv_M_2x2.LUSTREC.lus
diff --git a/lustrec_tests/minimal_tests_O1/test.ml b/lustrec_tests/minimal_tests/test.ml
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/test.ml
rename to lustrec_tests/minimal_tests/test.ml
diff --git a/lustrec_tests/minimal_tests_O1/two_counters.lus b/lustrec_tests/minimal_tests/two_counters.lus
similarity index 100%
rename from lustrec_tests/minimal_tests_O1/two_counters.lus
rename to lustrec_tests/minimal_tests/two_counters.lus
diff --git a/lustrec_tests/minimal_tests_O1/dune b/lustrec_tests/minimal_tests_O1/dune
deleted file mode 100644
index 954cbd74947b736bb97620da16e147000c65f48a..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O1/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O1")))
diff --git a/lustrec_tests/minimal_tests_O1/ignored b/lustrec_tests/minimal_tests_O1/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076d82ee615f7f9b6ca91a5ddc7d6f0ff54..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53da4d10e2e69d64c990cae687f81215af9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f7a54ef4031c8aaaf7ef2746066cf52b9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046754fefbf09e45a26f321d242c726e7fa..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea319dc79816d48fc73af1d92b818d1428e7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff24da7df2369c48c1cadd73917b352547..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9fc95a91db76c4360aac578cf350fbfeb5..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00999b632ec4a6faf05363e1ebfc3ad888..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f6465e6753d3c807e8605db8323b3e09c83..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/_6counter.lus b/lustrec_tests/minimal_tests_O2/_6counter.lus
deleted file mode 120000
index b146d803bdb59bca7beefc032449ce393af0d3da..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/clocks1.lus b/lustrec_tests/minimal_tests_O2/clocks1.lus
deleted file mode 120000
index b0c8f6291489739b43eac27937ae674167d55bd9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/dune b/lustrec_tests/minimal_tests_O2/dune
deleted file mode 100644
index 4a6e21ddb15415257ab0709634f0c83f8123c5c3..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O2")))
diff --git a/lustrec_tests/minimal_tests_O2/hysteresis_1.lus b/lustrec_tests/minimal_tests_O2/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a25034d033cddcb5d3a747b0bebda7e97..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/ignored b/lustrec_tests/minimal_tests_O2/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699f972afd6b9ba4644157f8cba6d1b253a..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O2/two_counters.lus b/lustrec_tests/minimal_tests_O2/two_counters.lus
deleted file mode 120000
index 65993869ee3ef38363cb58031abf254e1470adb7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O2/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076d82ee615f7f9b6ca91a5ddc7d6f0ff54..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53da4d10e2e69d64c990cae687f81215af9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f7a54ef4031c8aaaf7ef2746066cf52b9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046754fefbf09e45a26f321d242c726e7fa..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea319dc79816d48fc73af1d92b818d1428e7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff24da7df2369c48c1cadd73917b352547..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9fc95a91db76c4360aac578cf350fbfeb5..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00999b632ec4a6faf05363e1ebfc3ad888..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f6465e6753d3c807e8605db8323b3e09c83..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/_6counter.lus b/lustrec_tests/minimal_tests_O3/_6counter.lus
deleted file mode 120000
index b146d803bdb59bca7beefc032449ce393af0d3da..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/clocks1.lus b/lustrec_tests/minimal_tests_O3/clocks1.lus
deleted file mode 120000
index b0c8f6291489739b43eac27937ae674167d55bd9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/dune b/lustrec_tests/minimal_tests_O3/dune
deleted file mode 100644
index 770302df9ee66fb87430a8c35414291080ae8a69..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O3")))
diff --git a/lustrec_tests/minimal_tests_O3/hysteresis_1.lus b/lustrec_tests/minimal_tests_O3/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a25034d033cddcb5d3a747b0bebda7e97..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/ignored b/lustrec_tests/minimal_tests_O3/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699f972afd6b9ba4644157f8cba6d1b253a..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/test.ml b/lustrec_tests/minimal_tests_O3/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_O3/two_counters.lus b/lustrec_tests/minimal_tests_O3/two_counters.lus
deleted file mode 120000
index 65993869ee3ef38363cb58031abf254e1470adb7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_O3/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus
deleted file mode 120000
index c1d31076d82ee615f7f9b6ca91a5ddc7d6f0ff54..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Abs1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Abs1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus
deleted file mode 120000
index 3b92d53da4d10e2e69d64c990cae687f81215af9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Assignment1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Assignment1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus
deleted file mode 120000
index ccb3f23f7a54ef4031c8aaaf7ef2746066cf52b9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/BitwiseXOR_int8_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/BitwiseXOR_int8_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus
deleted file mode 120000
index 9b69e046754fefbf09e45a26f321d242c726e7fa..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Clock_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Clock_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus
deleted file mode 120000
index c25dea319dc79816d48fc73af1d92b818d1428e7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/ForEach1_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/ForEach1_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus
deleted file mode 120000
index 21a724ff24da7df2369c48c1cadd73917b352547..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/LookupTable1D_2points_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/LookupTable1D_2points_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus
deleted file mode 120000
index c44fcd9fc95a91db76c4360aac578cf350fbfeb5..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/Product1.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/Product1.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus b/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus
deleted file mode 120000
index 2bbb1f00999b632ec4a6faf05363e1ebfc3ad888..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/SYNAPSE_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/SYNAPSE_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus
deleted file mode 120000
index a5913f6465e6753d3c807e8605db8323b3e09c83..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/UnitDelay_PP.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/UnitDelay_PP.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus b/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus
deleted file mode 120000
index b146d803bdb59bca7beefc032449ce393af0d3da..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/_6counter.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/_6counter.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus b/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus
deleted file mode 120000
index b0c8f6291489739b43eac27937ae674167d55bd9..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/clocks1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/clocks1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/dune b/lustrec_tests/minimal_tests_wo_optimizations/dune
deleted file mode 100644
index fd6ebfc42e33e6b542ef98380f4c749c239e3876..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O-1")))
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus b/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus
deleted file mode 120000
index 15c1af9a25034d033cddcb5d3a747b0bebda7e97..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/hysteresis_1.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/hysteresis_1.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/ignored b/lustrec_tests/minimal_tests_wo_optimizations/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus b/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus
deleted file mode 120000
index 57753699f972afd6b9ba4644157f8cba6d1b253a..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/inv_M_2x2.LUSTREC.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/inv_M_2x2.LUSTREC.lus
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/test.ml b/lustrec_tests/minimal_tests_wo_optimizations/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus b/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus
deleted file mode 120000
index 65993869ee3ef38363cb58031abf254e1470adb7..0000000000000000000000000000000000000000
--- a/lustrec_tests/minimal_tests_wo_optimizations/two_counters.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/two_counters.lus
\ No newline at end of file
diff --git a/lustrec_tests/offline_tests/config.json b/lustrec_tests/offline_tests/config.json
new file mode 100644
index 0000000000000000000000000000000000000000..e22e16303acdbf24a6dab0724b42c486f8db4117
--- /dev/null
+++ b/lustrec_tests/offline_tests/config.json
@@ -0,0 +1,5 @@
+{
+ "initial_timeout": 30,
+ "optimization_level": 1,
+ "ignored_file": "ignored"
+}
diff --git a/lustrec_tests/offline_tests/dune b/lustrec_tests/offline_tests/dune
deleted file mode 100644
index 776c48563e79b4f8ed556601c93aa89adce57241..0000000000000000000000000000000000000000
--- a/lustrec_tests/offline_tests/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "offline_tests" 15360 "O2")))
diff --git a/lustrec_tests/offline_tests/dune b/lustrec_tests/offline_tests/dune
new file mode 120000
index 0000000000000000000000000000000000000000..55afef878ff2c0566e6fd92d804c17520ccc9a12
--- /dev/null
+++ b/lustrec_tests/offline_tests/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test/config.json b/lustrec_tests/stopwatch_test/config.json
new file mode 100644
index 0000000000000000000000000000000000000000..45a14ce0a184f47e71d833d3f416c2c77c65d07f
--- /dev/null
+++ b/lustrec_tests/stopwatch_test/config.json
@@ -0,0 +1,4 @@
+{
+ "initial_timeout": 60,
+ "optimization_level": 1
+}
diff --git a/lustrec_tests/stopwatch_test/dune b/lustrec_tests/stopwatch_test/dune
new file mode 120000
index 0000000000000000000000000000000000000000..55afef878ff2c0566e6fd92d804c17520ccc9a12
--- /dev/null
+++ b/lustrec_tests/stopwatch_test/dune
@@ -0,0 +1 @@
+../dune
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O1/simple_stopwatch.lus b/lustrec_tests/stopwatch_test/simple_stopwatch.lus
similarity index 100%
rename from lustrec_tests/stopwatch_test_O1/simple_stopwatch.lus
rename to lustrec_tests/stopwatch_test/simple_stopwatch.lus
diff --git a/lustrec_tests/minimal_tests_O2/test.ml b/lustrec_tests/stopwatch_test/test.ml
similarity index 100%
rename from lustrec_tests/minimal_tests_O2/test.ml
rename to lustrec_tests/stopwatch_test/test.ml
diff --git a/lustrec_tests/stopwatch_test_O1/dune b/lustrec_tests/stopwatch_test_O1/dune
deleted file mode 100644
index 9b92549361ad2ef89d35e0f5d6bfd3d584651225..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O1/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O1")))
diff --git a/lustrec_tests/stopwatch_test_O1/ignored b/lustrec_tests/stopwatch_test_O1/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/stopwatch_test_O1/test.ml b/lustrec_tests/stopwatch_test_O1/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O1/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O2/dune b/lustrec_tests/stopwatch_test_O2/dune
deleted file mode 100644
index a3f05791f8b8cb853c1d9ad86364e91b3f3478af..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O2/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O2")))
diff --git a/lustrec_tests/stopwatch_test_O2/ignored b/lustrec_tests/stopwatch_test_O2/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f2e2fec4de66c610990d7ca9d8a3e53df..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O2/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O2/test.ml b/lustrec_tests/stopwatch_test_O2/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O2/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O3/dune b/lustrec_tests/stopwatch_test_O3/dune
deleted file mode 100644
index 58e70106b800a214b0a8ec46934f97a492927790..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O3/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O3")))
diff --git a/lustrec_tests/stopwatch_test_O3/ignored b/lustrec_tests/stopwatch_test_O3/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f2e2fec4de66c610990d7ca9d8a3e53df..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O3/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_O3/test.ml b/lustrec_tests/stopwatch_test_O3/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_O3/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/dune b/lustrec_tests/stopwatch_test_wo_optimizations/dune
deleted file mode 100644
index 6dc4eac5b0a971c6f83b94accbae0756d43b7eb6..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/dune
+++ /dev/null
@@ -1,13 +0,0 @@
-(env
- (dev
- (flags (:standard -w -32))))
-
-(test
- (name test)
- (libraries re unix yojson)
- (deps
- (:lus
- (glob_files *.lus))
- (:ign ignored))
- (action
- (run %{test} %{bin:lustrec} "%{lus}" %{ign} "stopwatch_test" 60 "O-1")))
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/ignored b/lustrec_tests/stopwatch_test_wo_optimizations/ignored
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus b/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus
deleted file mode 120000
index b83efd7f2e2fec4de66c610990d7ca9d8a3e53df..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/simple_stopwatch.lus
+++ /dev/null
@@ -1 +0,0 @@
-../lustre_files/simple_stopwatch.lus
\ No newline at end of file
diff --git a/lustrec_tests/stopwatch_test_wo_optimizations/test.ml b/lustrec_tests/stopwatch_test_wo_optimizations/test.ml
deleted file mode 120000
index 9536c050ab0df996b8dc9f282da649b234ebd99b..0000000000000000000000000000000000000000
--- a/lustrec_tests/stopwatch_test_wo_optimizations/test.ml
+++ /dev/null
@@ -1 +0,0 @@
-../test.ml
\ No newline at end of file
diff --git a/lustrec_tests/test.ml b/lustrec_tests/test.ml
index 61688931bc1f3874544ac181cd9408589389e8d6..c7b9c6e5bc164db1f281fc79bae2fe842d19fdb4 100644
--- a/lustrec_tests/test.ml
+++ b/lustrec_tests/test.ml
@@ -1,6 +1,8 @@
open Format
open Unix
+module Y = Yojson.Basic
+
module S = struct
include Set.Make (String)
@@ -52,29 +54,22 @@ let empty_report =
ninits = S.empty;
}
-let initial_timeout = int_of_string Sys.argv.(5)
-let optimization_level = match Sys.argv.(6) with
- | "O2" -> None
- | "O-1" -> Some (-1)
- | "O1" -> Some 1
- | "O3" -> Some 3
- | _ -> failwith
- "optimization option not supported. Choose between O-1, O1, O2, O3"
-let result_dir = "../../../../results/"
-let _ = try Unix.mkdir result_dir 0o755 with _ -> ()
-let dir = result_dir ^ Sys.argv.(4) ^ "_" ^
- match Sys.argv.(6) with
- | "O-1" -> "wo_optimizations"
- | other -> other
-let _ = try Unix.mkdir dir 0o755 with _ -> ()
-let report_f = Filename.concat dir "report"
+type config = {
+ initial_timeout: int;
+ optimization_level: int;
+ ignored_file: string option;
+ results_directory: string;
+}
+
+let report_file cfg = Filename.concat cfg.results_directory "report"
+
let section h = "# " ^ h
let end_section = "##"
let compiled_section = section "COMPILED"
let ninit_section = section "BAD_INIT"
-let next_timeout r =
- 2 * M.fold (fun i _ n -> max i n) r.verified (initial_timeout / 2)
+let next_timeout cfg r =
+ 2 * M.fold (fun i _ n -> max i n) r.verified (cfg.initial_timeout / 2)
let timeout_section i = section (sprintf "TIMEOUT %d" i)
@@ -111,9 +106,9 @@ let is_failed report f = STF.exists (fun (x, _) -> x = f) report.failed
let add_failed report ?goals f =
{ report with failed = STF.add (f, goals) report.failed }
-let parse_report () =
+let parse_report cfg =
try
- let ic = open_in report_f in
+ let ic = open_in (report_file cfg) in
let rec read_compiled r =
try
match input_line ic with
@@ -229,8 +224,8 @@ let pp_report fmt report =
pp_verified
report
-let write_report report =
- let oc = open_out report_f in
+let write_report cfg report =
+ let oc = open_out (report_file cfg) in
let fmt = formatter_of_out_channel oc in
pp_report fmt report;
close_out oc
@@ -279,14 +274,15 @@ let print_result p f fmt_str check =
let print_results ok ko w n =
printf "OK: @{<green>%d@} (@{<red>%d@} + @{<magenta>%d@}) / %d@." ok ko w n
-let lustrec_params f =
- let ps = [ "-acsl-spec"; "-d"; dir; f ] in
- Option.fold
- ~none:ps
- ~some:(fun x -> "-O" :: string_of_int x :: ps)
- optimization_level
+let lustrec_params cfg f =
+ [
+ "-acsl-spec";
+ "-d"; cfg.results_directory;
+ "-O"; cfg.optimization_level |> string_of_int;
+ f
+ ]
-let compile report lustrec fs =
+let compile cfg report lustrec fs =
printf "@.%a@." pp_header "Compilation tests";
max_l :=
List.fold_left
@@ -316,7 +312,7 @@ let compile report lustrec fs =
else if is_ninit report f then ninit report
else
let cmd =
- Filename.quote_command ~stderr:err_f lustrec (lustrec_params f)
+ Filename.quote_command ~stderr:err_f lustrec (lustrec_params cfg f)
in
let ic = open_process_in cmd in
let b =
@@ -329,7 +325,7 @@ let compile report lustrec fs =
else fail report log
in
print_result p f fmt_str check;
- write_report report;
+ write_report cfg report;
report, ok, ko, ninits, i')
(report, 0, 0, 0, 0)
fs
@@ -429,7 +425,7 @@ let rec rmrf path =
else Sys.remove path
with _ -> ()
-let rec verify report timeout fs =
+let rec verify cfg report timeout fs =
if fs <> [] then (
printf
"@.%a@."
@@ -441,7 +437,7 @@ let rec verify report timeout fs =
List.fold_left
(fun (report, ok, ko, tm, i, fs) f ->
let f' = Filename.remove_extension f ^ ".c" in
- let f'' = Filename.concat dir f' in
+ let f'' = Filename.concat cfg.results_directory f' in
let i' = i + 1 in
let p = float_of_int i' *. 100. /. n_f in
let success ?(already = false) r : _ * _ * _ * _ * _ format * _ * _ =
@@ -495,35 +491,66 @@ let rec verify report timeout fs =
fail (add_failed report f'))
in
print_result p f' fmt_str check;
- write_report report;
+ write_report cfg report;
report, ok, ko, tm, i', fs)
(report, 0, 0, 0, 0, [])
fs
in
print_results ok ko tm n;
- verify report (timeout * 2) fs)
+ verify cfg report (timeout * 2) fs)
let print_ignored fs =
- printf
- "@.@[<v 2>%a@;%a@]@."
- pp_header
- "Ignored tests"
- (pp_print_list pp_print_string)
- fs
+ if fs <> [] then
+ printf
+ "@.@[<v 2>%a@;%a@]@."
+ pp_header
+ "Ignored tests"
+ (pp_print_list pp_print_string)
+ fs
+
+let read_config root =
+ let open Yojson.Basic.Util in
+ let json = Sys.argv.(3) |> Y.from_file in
+ let get field f = json |> member field |> f in
+ let get_default field f default =
+ Option.fold ~none:default ~some:Fun.id (get field (to_option f))
+ in
+ let tests_directory = Sys.getcwd () |> Filename.basename in
+ let optimization_level = get_default "optimization_level" to_int 2 in
+ let result_dir = root ^ "/../../results/" in
+ (try Unix.mkdir result_dir 0o755 with _ -> ());
+ let results_directory =
+ result_dir ^ tests_directory ^ "_" ^
+ (if optimization_level < 0 then "wo_optimization"
+ else "O" ^ string_of_int optimization_level)
+ in
+ (try Unix.mkdir results_directory 0o755 with _ -> ());
+ {
+ initial_timeout = get_default "initial_timeout" to_int 30;
+ optimization_level;
+ results_directory;
+ ignored_file = get "ignored_file" to_string_option;
+ }
let () =
- let lustrec = Sys.argv.(1) in
- let lus_fs = Sys.argv.(2) |> Re.Str.(split (regexp_string " ")) in
- let ignored_f = Sys.argv.(3) in
+ let root = Sys.argv.(1) in
+ let lustrec = Sys.argv.(2) in
+ let cfg = read_config root in
+ let lus_fs = Sys.argv.(4) |> Re.Str.(split (regexp_string " ")) in
let ignored_fs =
- let ic = open_in ignored_f in
- let rec read fs = try read (input_line ic :: fs) with End_of_file -> fs in
- let fs = read [] in
- close_in ic;
- fs
+ Option.fold ~none:[]
+ ~some:(fun ignored_f ->
+ let ic = open_in ignored_f in
+ let rec read fs =
+ try read (input_line ic :: fs) with End_of_file -> fs
+ in
+ let fs = read [] in
+ close_in ic;
+ fs)
+ cfg.ignored_file
in
- let report = parse_report () in
- let report = compile report lustrec lus_fs in
+ let report = parse_report cfg in
+ let report = compile cfg report lustrec lus_fs in
let ignored_fs =
ignored_fs @ List.map Filename.chop_extension (S.elements report.ninits)
in
@@ -536,4 +563,4 @@ let () =
(fun f -> not (mem (Filename.chop_extension f) ignored_fs))
lus_fs))
in
- verify report (next_timeout report) lus_fs
+ verify cfg report (next_timeout cfg report) lus_fs