Merge branch 'master' of github.com:DavePearce/Whiley into devel-smt
WyCS: Bug fix for #400.
There was a misssing case in Solve$native.compare().  In fact, I've now
simplified to reduce the number of cases by exploiting Constant as a
common supertype to e.g. Int, Bool, Real, etc.
WyRL: Performance optimisation for probe().
Whilst invesigating #400, I noticed that there were some unnecessary
loops in the probe() function.  Essentially for cases where we didn't
need to further check a pattern, since it was guaranteed to be its
declared type.  This is now fixed, though unclear whether it's made any
useful performance improvement.
WyRL: Bug fix for #403.
A situation existed where the reachable information maintained by
IterativeRewriter could get out of sync after a minimise() operation was
made.  This is now fixed, though it could be more efficient.
WyCS: Bug fix for problem similar to that in #400
WyCS: Bug fix for #404.
However, although this bug fix works, I'm going to make it more
efficient still.
WyCS: Performance Improvement for #404.
The previous rule used to fix #404 was less than efficient, and I've now
replaced it with something a little smarter.
WyCS: Added Test Case for #401.
A very simple test case was missing, apparently.
WyCS: Bug fix for #401.
This was relatively easy to fix, and was essentially just missing a rule
in the verifier.  Very surprised I hadn't found this before though.
WyCS: Uncommented some test cases which now pass.
As a result of various bug fixes (e.g. #401, #403, #400, #404) some
additional test cases are now passing which previously were not.
TEST: added missing test output.
WyC: Return stmt check for missing value. #395
Previously, the flow type checker did not ensure that, for a function or
method declared to return a value, when a return statement was
encountered that it actually returned a value.  This is now fixed, and
the error reported mimics Java "missing return value".
WyC: Possible fix for #395.
The compiler now reports "missing return statement" in the case of a
function or method which is declared to return a value, and for which
there is an execution path through it which does not end with a return
statement.  Unfortunately, there are some test cases failing as a result
of this which need to be further investigated before closing the issue.
WyC: Fix for type checking Switch statements #395
The flow type checker was not correctly typing the cases of a switch
statement.  This only became apparent through the fix for #395, which
exposed the fact than a non-empty environment was still being returned
even when no possible branches could exit the switch.
TESTING: Added missing test case outputs.
Some tests were missing their sample output files and I didn't notice.
Now corrected.
WyC: Tidied up some test cases.
Several test cases were failing to compile for various reasons, mostly
because of bugs (e.g. #406).  I've now tidied this up by @Ignoring them
and/or fixing what was necessary.
WyC: added new test cases and output.
Merge branch 'master' of github.com:DavePearce/Whiley
WyBS: Updated brief-mode error reporting.
This is to allow Whiley play to better report multi-line errors.  Previously, such errors were causing some confusion within Whiley play and leading to confusing error messages.
TESTING: Marked more test cases with @Ignore.
These test cases are failing for the issue outlined in #406.  They are
marked as ignore now because they aren't likely to be fixed in the near
future.