Skip to content

Commit

Permalink
Adds regression test for dumptests.
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
benjaminselfridge committed Nov 2, 2020
1 parent ec5a504 commit fdd7aab
Show file tree
Hide file tree
Showing 4 changed files with 9 additions and 0 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,4 @@ cryptol-2.*
# ignore test suite output
/bin
/output
/tests/regression/*.out
2 changes: 2 additions & 0 deletions tests/regression/dumptests.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
add32 : [32] -> [32] -> [32]
add32 x y = x + y
3 changes: 3 additions & 0 deletions tests/regression/dumptests.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
:set tests=100
:l dumptests.cry
:dumptests add32.out add32
3 changes: 3 additions & 0 deletions tests/regression/dumptests.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main

0 comments on commit fdd7aab

Please sign in to comment.