Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

1 files changed, 16 insertions, 2 deletions

diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
index d21a46fc..819081a2 100644
--- a/tests/test_runner/Backend.ml
+++ b/tests/test_runner/Backend.ml
@@ -1,15 +1,24 @@
 (*** Define the backends we support as an enum *)
 
-type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
+type t =
+  | Coq
+  | Lean
+  | FStar
+  | HOL4
+  | BorrowCheck
+      (** Borrow check: no backend.
+          We use this when we only want to borrow-check the program *)
+[@@deriving ord, sexp]
 
 (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-let all = [ Coq; Lean; FStar ]
+let all = [ Coq; Lean; FStar; BorrowCheck ]
 
 let of_string = function
   | "coq" -> Coq
   | "lean" -> Lean
   | "fstar" -> FStar
   | "hol4" -> HOL4
+  | "borrow-check" -> BorrowCheck
   | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
 
 let to_string = function
@@ -17,6 +26,11 @@ let to_string = function
   | Lean -> "lean"
   | FStar -> "fstar"
   | HOL4 -> "hol4"
+  | BorrowCheck -> "borrow-check"
+
+let to_command = function
+  | BorrowCheck -> [ "-borrow-check" ]
+  | x -> [ "-backend"; to_string x ]
 
 module Map = struct
   (* Hack to be able to include things from the parent module with the same names *)