summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
Diffstat (limited to 'tests/test_runner')
-rw-r--r--tests/test_runner/.ocamlformat0
-rw-r--r--tests/test_runner/aeneas_test_runner.opam27
-rw-r--r--tests/test_runner/dune4
-rw-r--r--tests/test_runner/dune-project25
-rw-r--r--tests/test_runner/run_test.ml30
5 files changed, 86 insertions, 0 deletions
diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/tests/test_runner/.ocamlformat
diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
new file mode 100644
index 00000000..b57cc9f6
--- /dev/null
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -0,0 +1,27 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+authors: ["Son Ho" "Guillaume Boisseau"]
+license: "Apache-2.0"
+homepage: "https://github.com/AeneasVerif/aeneas"
+bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
+depends: [
+ "ocaml"
+ "dune" {>= "3.12"}
+ "odoc" {with-doc}
+]
+build: [
+ ["dune" "subst"] {dev}
+ [
+ "dune"
+ "build"
+ "-p"
+ name
+ "-j"
+ jobs
+ "@install"
+ "@runtest" {with-test}
+ "@doc" {with-doc}
+ ]
+]
+dev-repo: "git+https://github.com/AeneasVerif/aeneas.git"
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
new file mode 100644
index 00000000..7da7a96d
--- /dev/null
+++ b/tests/test_runner/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name test_runner)
+ (libraries unix)
+ (name run_test))
diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
new file mode 100644
index 00000000..c614e923
--- /dev/null
+++ b/tests/test_runner/dune-project
@@ -0,0 +1,25 @@
+(lang dune 3.12)
+
+(name aeneas_test_runner)
+
+(version 0.1)
+
+(generate_opam_files true)
+
+(source
+ (uri git+https://github.com/AeneasVerif/aeneas.git))
+
+(homepage "https://github.com/AeneasVerif/aeneas")
+
+(bug_reports "https://github.com/AeneasVerif/aeneas/issues")
+
+(authors
+ "Son Ho"
+ "Guillaume Boisseau")
+
+(license Apache-2.0)
+
+(package
+ (name aeneas_test_runner)
+ (depends ocaml dune)
+)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
new file mode 100644
index 00000000..379abe04
--- /dev/null
+++ b/tests/test_runner/run_test.ml
@@ -0,0 +1,30 @@
+let concat_path = List.fold_left Filename.concat ""
+
+let () =
+ match Array.to_list Sys.argv with
+ (* Ad-hoc argument passing for now. *)
+ | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend
+ :: options ->
+ let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in
+ let dest_dir = concat_path [ "tests"; backend; subdir ] in
+ let args =
+ [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
+ in
+ let args = Array.append args (Array.of_list options) in
+
+ (* Debug arguments *)
+ print_string "[test_runner] Running: ";
+ Array.iter
+ (fun x ->
+ print_string x;
+ print_string " ")
+ args;
+ print_endline "";
+
+ (* Run Aeneas *)
+ let pid =
+ Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+ in
+ let _ = Unix.waitpid [] pid in
+ ()
+ | _ -> ()