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.
This commit is contained in:
Ben Selfridge 2020-11-02 13:59:22 -08:00
parent ec5a50436a
commit fdd7aab01a
4 changed files with 9 additions and 0 deletions

1
.gitignore vendored
View File

@ -30,3 +30,4 @@ cryptol-2.*
# ignore test suite output
/bin
/output
/tests/regression/*.out

View File

@ -0,0 +1,2 @@
add32 : [32] -> [32] -> [32]
add32 x y = x + y

View File

@ -0,0 +1,3 @@
:set tests=100
:l dumptests.cry
:dumptests add32.out add32

View File

@ -0,0 +1,3 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main