Update the test architecture to handle JSON config

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:
 

lustrec_tests/minimal_tests_O1/dune → lustrec_tests/dune

@@ -6,8 +6,8 @@
  (name test)
  (libraries re unix yojson)
  (deps
-  (:lus
-   (glob_files *.lus))
-  (:ign ignored))
+  (:lus (glob_files *.lus))
+  (:cfg config.json)
+  (glob_files *))               ; to include `ignored` if its present
  (action
-  (run %{test} %{bin:lustrec} "%{lus}" %{ign} "minimal_tests" 240 "O1")))
+  (run %{test} %{project_root} %{bin:lustrec} %{cfg} "%{lus}")))

lustrec_tests/minimal_tests/config.json

+{
+    "initial_timeout": 240,
+    "optimization_level": 1,
+    "ignored_file": null
+}

lustrec_tests/minimal_tests/dune

+../dune
\ No newline at end of file