From fdd7aab01aaebcb68d88f5f4d2bde0c0f2c2bb75 Mon Sep 17 00:00:00 2001
From: Ben Selfridge <benselfridge@galois.com>
Date: Mon, 2 Nov 2020 13:59:22 -0800
Subject: [PATCH] Adds regression test for dumptests.

This only checks that a function with signature [32] -> [32] -> [32] will
succeed with the :dumptests command. More tests could/should be added.

Since this test creates a file called add32.out, I added tests/regression/*.out
to the .gitignore. I'm not sure if this is the right approach or if we should
make an attempt to clean up this subdirectory after the tests finish.
---
 .gitignore                             | 1 +
 tests/regression/dumptests.cry         | 2 ++
 tests/regression/dumptests.icry        | 3 +++
 tests/regression/dumptests.icry.stdout | 3 +++
 4 files changed, 9 insertions(+)
 create mode 100644 tests/regression/dumptests.cry
 create mode 100644 tests/regression/dumptests.icry
 create mode 100644 tests/regression/dumptests.icry.stdout

diff --git a/.gitignore b/.gitignore
index a73fa768..8827bc1d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -30,3 +30,4 @@ cryptol-2.*
 # ignore test suite output
 /bin
 /output
+/tests/regression/*.out
diff --git a/tests/regression/dumptests.cry b/tests/regression/dumptests.cry
new file mode 100644
index 00000000..0427fb34
--- /dev/null
+++ b/tests/regression/dumptests.cry
@@ -0,0 +1,2 @@
+add32 : [32] -> [32] -> [32]
+add32 x y = x + y
\ No newline at end of file
diff --git a/tests/regression/dumptests.icry b/tests/regression/dumptests.icry
new file mode 100644
index 00000000..369d882e
--- /dev/null
+++ b/tests/regression/dumptests.icry
@@ -0,0 +1,3 @@
+:set tests=100
+:l dumptests.cry
+:dumptests add32.out add32
\ No newline at end of file
diff --git a/tests/regression/dumptests.icry.stdout b/tests/regression/dumptests.icry.stdout
new file mode 100644
index 00000000..57a1d7a1
--- /dev/null
+++ b/tests/regression/dumptests.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main