The Smtlib solver was translating Fin constraints to True, as it didn't know
how to handle them. They should have been skipped, and returned back as
unsolved goals instead.
This tries to address #125 by making the errors from the renamer a little bit
more clear.
Squashed commit of the following:
commit 8afd3d7961b58df042fe801c3c5e1b9787f813bc
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:59 2014 -0800
Update tests for new renamer errors
commit 7cac01836d8943cf3b08d6715ac328e3b6658cef
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:49 2014 -0800
Add `at` on errors and warnings to be more consistent
commit 308908ba318a4cdc839710f66f1a487543f8c07e
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:06:57 2014 -0800
More consistent renamer warnings
commit be8100a78e9eaba6d554591121c24ed5dcd3c780
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:53 2014 -0800
More consistent error formatting from the renamer
commit 26c45c3b51e0bdbcf6a1431cab8e1eb8760ea0bb
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:36 2014 -0800
Remove an un-triggerable error
commit ccdb93e036ba1e111ccd977c8b3b35523f3c1bf0
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:44 2014 -0800
Try to give better errors for unbound identifiers
commit eb5784145985bb55c761088eaba27c67d08c1326
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:23 2014 -0800
Remove old TODOs about located errors
commit b984bb5f451f3aa7b4fc8f15167483c5142ee9a3
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:37:34 2014 -0800
Differentiate missing type and expression symbols
commit b9e6f13856db6765dced3cb9565cdc8387a7976d
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:36:52 2014 -0800
Remove a shadowing warning
Due to the limitations of the GHC runtime, we can't get around the
possibility of out-of-memory errors, but we can prevent individual
bitvectors from being too large for the libgmp-backed bignums.
There is now an architecture-dependent check whenever creating a new
`BV` value in the concrete evaluator to ensure the width does not
exceed the GMP limits. If a width is too large, the evaluation returns
to the REPL much like diving by zero.
Previously it would try to convert the recursive value directly
into a VWord constructor, forcing all bits immediately and causing
non-termination. Now it produces a VSeq constructor instead.
This addresses issue #130.
This "fix" adds two locations to the search path for Cryptol modules so that we can find the prelude on both Windows and Unix platforms. This is not ideal and should be replaced in the next version, but should have no negative impact for now unless people have multiple Cryptol.cry files hanging out in their filesystems.
Previously, if one command was a prefix of another command, that would lead to an ambiguous lookup from the command trie. Now there are two ways to look up: one works like previously, which is good for tab-completion, and the other will only return one result if there is an exact match.
This means we can now have multiple forms of each command, so we can explicitly have short forms like :e -> :edit that won't be changed just based on what names we give to future commands.
This closes#90, and also #94 which was blocked on this due to :exhaust and :edit conflicting.
To mark a failing test as a known failure, you should add a file with
a name like this:
TESTNAME.icry.fails
When the test runs, if it fails, then the contents of this file is displayed.
It is a probably a good idea for the contents to reference the ticket where
the failure was reported.
When the problem is fixed, the `.fails` should be removed. Failing to do
so will result in test failure (i.e., a test that passes but has a `.fails`
file is considered an error).
