From c6f70bff7a70c7681462a1fb3bcddd9f1adf1b50 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Fri, 14 Jul 2023 18:26:01 +0100
Subject: [PATCH] CN: add a test runner

A very simple shell-script will run the tests in the tests/cn
directory and report success or failure in its final return
value.
---
 backend/cn/main.ml | 15 +++++++++++----
 tests/run-cn.sh    | 28 ++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 4 deletions(-)
 create mode 100644 tests/run-cn.sh

diff --git a/backend/cn/main.ml b/backend/cn/main.ml
index 5cba93030..89f2eca70 100644
--- a/backend/cn/main.ml
+++ b/backend/cn/main.ml
@@ -119,6 +119,7 @@ let main
       solver_logging
       output_decorated
       astprints
+      expect_failure
   =
   if json then begin
       if debug_level > 0 then
@@ -185,9 +186,10 @@ let main
        in
        Pp.maybe_close_times_channel ();
        match result with
-       | Ok () -> exit 0
-       | Error e when json -> TypeErrors.report_json ?state_file e; exit 1
-       | Error e -> TypeErrors.report ?state_file e; exit 1
+       | Ok () -> exit (if expect_failure then 1 else 0)
+       | Error e ->
+         if json then TypeErrors.report_json ?state_file e else TypeErrors.report ?state_file e;
+         exit (if expect_failure then 0 else 1)
  with
      | exc -> 
         Cerb_debug.maybe_close_csv_timing_file ();
@@ -292,6 +294,10 @@ let astprints =
   Arg.(value & opt (list (enum [("cabs", Cabs); ("ail", Ail); ("core", Core); ("types", Types)])) [] &
        info ["ast"] ~docv:"LANG1,..." ~doc)
 
+let expect_failure =
+  let doc = "invert return value to 1 if type checks pass and 0 on failure" in
+  Arg.(value & flag & info["expect-failure"] ~doc)
+
 
 let () =
   let open Term in
@@ -316,6 +322,7 @@ let () =
       random_seed $
       solver_logging $
       output_decorated $
-      astprints
+      astprints $
+      expect_failure
   in
   Stdlib.exit @@ Cmd.(eval (v (info "cn") check_t))
diff --git a/tests/run-cn.sh b/tests/run-cn.sh
new file mode 100644
index 000000000..fb72ca7e5
--- /dev/null
+++ b/tests/run-cn.sh
@@ -0,0 +1,28 @@
+#! /bin/bash
+
+# tests for the CN tool attached to cerberus
+
+DIRNAME=$(dirname $0)
+
+set -e
+
+SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.wrong\.c')
+
+for TEST in $SUCC
+do
+  echo cn $TEST
+  cn $TEST
+done
+
+FAIL=$(find $DIRNAME/cn -name '*.wrong.c')
+
+for TEST in $FAIL
+do
+  echo cn --expect-fail $TEST
+  cn --expect-failure $TEST
+done
+
+echo "All tests passed."
+
+return 0
+