GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-23 22:27:25 +03:00
Code Issues Projects Releases Wiki Activity
2,305 Commits 68 Branches 28 Tags 95 MiB
5f86556c5c
Commit Graph

335 Commits

Author SHA1 Message Date
David Thrane Christiansen
02dfc4a898 Enforce that includes are UTF8 
Previously, "include" used locale-dependent decoding of source files,
while the rest of Cryptol uses UTF8. This change makes "include"
consistent with the rest of Cryptol, and adds a test that checks for
malformed UTF8.
 2020-06-09 09:02:22 -07:00
Rob Dockins
721e733ce9 yet more shifting fixes 2020-06-03 18:45:42 -07:00
Rob Dockins
acbf925afa Add a test case for shifting and rotating by negative integer values. 2020-06-03 17:55:50 -07:00
Rob Dockins
88c98c4c03 Merge remote-tracking branch 'origin/master' into split-arith 
Minor merge conflicts resolved.
 2020-06-03 13:35:04 -07:00
Andrei Stefanescu
2ff4d4c031
Fix Array.cry comment. (#748) 2020-06-02 20:26:49 -07:00
Rob Dockins
d816d8820a Tweak the test suite. Apparently echo works differently on Windows 2020-05-27 13:50:00 -07:00
Rob Dockins
066cbd492e Post-merge test suite fixups 2020-05-26 17:45:42 -07:00
Rob Dockins
bbba626052 Merge remote-tracking branch 'origin/master' into split-arith 2020-05-26 17:37:00 -07:00
Rob Dockins
c1b641c420 Add a test case for issue725 2020-05-26 17:08:20 -07:00
Rob Dockins
aaf78e23ec Add a bit more output for the Satisfiable/Counterexample cases 2020-05-26 17:08:20 -07:00
Rob Dockins
e817f5c777 Update test suite 2020-05-26 15:33:46 -07:00
Rob Dockins
85e49a92db Rearrange the Cryptol prelude according to the new typeclass system 2020-05-22 15:39:38 -07:00
Brian Huffman
37f1fd8b4b Add regression test for #731. 2020-05-18 17:17:58 -07:00
Rob Dockins
f6e0342afa Partially update the test suite 2020-05-15 09:33:32 -07:00
Brian Huffman
700b31803c Add regression test for #723. 2020-05-15 07:36:11 -07:00
Rob Dockins
6b961929a6 Add properties for rationals that specify correctness for the 
various properties of the Q and it's operations.
 2020-05-14 17:50:56 -07:00
Brian Huffman
9424752b45 Specialize types of signed div/mod operators (/$) and (%$) to bitvectors. 2020-05-13 17:19:18 -07:00
Iavor Diatchki
c3eca4f22a Check that the declared type of prims matches the expected one. 
Fixes #711
 2020-05-05 14:30:25 -07:00
robdockins
f29f0158ff
Merge pull request #703 from GaloisInc/issue702 
issue702
 2020-04-23 12:22:25 -07:00
Brian Huffman
4dd77c756b Update type variable numbering in test suite output. 2020-04-20 11:29:49 -07:00
Rob Dockins
ce85155dbe Add unit test for issue702 2020-04-17 17:48:44 -07:00
robdockins
87ad864185
Merge pull request #684 from GaloisInc/eval-refactor 
Evaluator refactor
 2020-04-02 09:42:04 -07:00
Rob Dockins
d08046d063 Test case for issue #662 2020-04-02 09:40:44 -07:00
Rob Dockins
943e11478a Add regression test for word updates 2020-03-30 15:09:53 -07:00
Iavor Diatchki
fcc7a19998 More information when browsing. 
This implements the feature request in #689
 2020-03-24 16:53:48 -07:00
Rob Dockins
f016a9a9fc Define carry and scarry instead of making them primitive. 2020-03-17 13:25:39 -07:00
Iavor Diatchki
3038eacf54 Add a test for record updating. 
This completes the implementation of record updates.
Fixes #399
 2020-01-21 11:35:19 -08:00
Kevin Quick
578d268b8e
Update cryptol-test-runner maintainer and license 2019-12-23 18:18:54 -08:00
Brian Huffman
aec6cb0a7e Add regression test for #670. 2019-12-16 18:02:56 -08:00
Brian Huffman
3281e7c121 Revert "Add regression test for #444." 
This reverts commit 85bff672ef.

The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.

Fixes #673.
 2019-12-16 14:12:44 -08:00
Brian Huffman
4b29967315 Add regression test for issue #614. 2019-12-13 11:13:03 -08:00
Brian Huffman
4da0f19a21 Add regression test for #667. 2019-12-06 15:51:57 -08:00
Brian Huffman
c230e2395c Use Data.Map to normalize record field order in Value type. 
Fixes #667.
 2019-12-06 15:48:50 -08:00
Brian Huffman
67fc36764c Add regression test for #664. 2019-11-26 22:23:53 -08:00
Brian Huffman
85bff672ef Add regression test for #444. 2019-11-21 06:04:27 -08:00
Aaron Tomb
ddbd664326
Merge pull request #655 from GaloisInc/at-ghc-881 
Fix build with GHC 8.8

Also updates CI to use GHC 8.4, 8.6, and 8.8 on both Travis and AppVeyor, and makes some small tweaks to make the tests pass in all six configurations.
 2019-11-01 13:56:05 -07:00
Aaron Tomb
82d4a1b81a Fix test output for issues/allexamples 2019-11-01 12:28:13 -07:00
Aaron Tomb
47b2eccad7 Remove leading ./ from file names in test output 2019-10-28 13:57:37 -07:00
Aaron Tomb
3ea5e9e51c Make issue072 test more robust to solver versions 2019-10-25 11:39:31 -07:00
Iavor Diatchki
8fe9f5efa9 Add support for working with in-memory sources. 
Currently we only use this for the Prelude, which is baked into Cryptol.
Previously we used to save it in a temporary file, which would show
up in error messages, leading to bad user experience and unreliable
test outputs.

Also improves the shadowing errors.

Fixes #569
 2019-07-05 14:09:04 -07:00
Iavor Diatchki
ca4968ff3d Fix test. The error message changed, but is still valid. 
We should really have only one way to say this,
I made a ticket: #633
 2019-07-05 09:37:45 -07:00
Iavor Diatchki
4b5d569e09 Fix tests---some variables got renumbered. 
We really should fix this up so we don't print the numbers unless
there really is an ambiguity.
 2019-07-05 09:34:20 -07:00
Iavor Diatchki
72068cb961 Move type-level primitives to the Prelude. 
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
 2019-07-02 17:34:36 -07:00
Iavor Diatchki
1cfadef5ea Add a forgotten test 2019-07-01 10:26:39 -07:00
Brian Huffman
1e11ff6b8b Add type constraint synonyms (<) and (>). 
Fixes #400.
 2019-06-26 20:44:13 -07:00
Brian Huffman
14d25e8f9a Fix pretty printing for infix type/constraint synonyms. 2019-06-26 18:19:12 -07:00
Brian Huffman
10da255fd1 Re-implement infix type constraint (<=) as a constraint synonym. 
Also removed special-case hack for (<=) in the renamer.

Also adapted test case output to account for the new prelude declaration.
 2019-06-26 18:04:16 -07:00
Brian Huffman
0a1cea2912 Update test suite output to accommodate new prelude function. 2019-06-18 15:39:56 -07:00
Iavor Diatchki
ec7c9a0f6e Don't generalize a rec. group, if any members are marked as monomorphic. 
Fixes #607
 2019-06-14 16:14:14 -07:00
Iavor Diatchki
08c537122a Update nQueens example to not print the found solution. 2019-03-25 16:20:17 -07:00