WyC,WyIL,WyjC: Added an AssertBlock bytecode #377.
The purpose of this bytecode is as a stepping stone towards bytecode
blocks (#190).  Furthermore, to remove the e.g. assertge bytecodes, and
replace them with fail bytecodes.  This should reduce the number of path
generated during verification condition generation.
WyC: Deleted CodeGenerator.
This class represents the future.  Unfortunately, there are two many
pressing changes that I need to push through that I cannot maintain it.
Therefore, I'm deleting it and I will simply need to regenerate it from
the OldCodeGenerator at some point in the future.
WyC: Deleted CodeGenerator.
This class represents the future.  Unfortunately, there are two many
pressing changes that I need to push through that I cannot maintain it.
Therefore, I'm deleting it and I will simply need to regenerate it from
the OldCodeGenerator at some point in the future.
WyC,WyIL,WyJC: Added AssumeBlock Bytecode #377.
As part of the move towards bytecode blocks, and the use of fail inplace
of e.g. assertge bytecodes, I have implemented the AssumeBlock bytecode.
WyC,WyIL: Removed assertge and related bytecodes.
This is not yet finished, as I need to plumb through a number of other
important fixes to the CodeGenerator and related pieces.
Merge branch 'devel-assert' of github.com:Whiley/WhileyCompiler into devel-assert
WyC,WyIL,WyJC: Removed assertXX bytecodes #377.
These bytecodes are now replaced with Assert blocks and Fail bytecodes.
This transformation is not yet complete.  Specifically, I still need to:
a) fixup DecisionTree; b) put back in loop invariants and
pre/post-conditions; c) make sure inlined invariants are put into an
Assert block.
WyC: Added missing file.
Merge branch 'master' into devel-assert

Conflicts:
	modules/wyc/src/wyc/builder/FlowTypeChecker.java
WyIL: Updated DecisionTree and VcBranch #377.

Updated DecisionTree so that it now correctly chains constraints
together.  Also, updated VcBranch and VcTransformer to recognise the new
assert block.
WyCS: Updated VcTransformer to check asserts #377.

The VcTransformer now translates Code.Fail bytecodes into assertions and
checks them.  This is not complete yet, since it should be decided
whether or not to assume them.
WyCS: Updated documentation.

Updated some documentation and removed some old commented out code.
WyC: Updated CodeGenerator for Various Invariants.

After the introduction of the new Assert and Assume blocks, the
CodeGenerator has now been updated to create appropriate assert and
assume blocks for loop invariants and pre/post-conditions.
WyIL: Working on getting the asserts vs assumptions to work.
WyIL: Finished Updating Verifier for Assert Blocks

Assert blocks are now implemented and working for #377.  Unfortunately,
getting them to work has been something of a hack and the verifier
really needs significant reworking to account for this.  In particular,
it needs to explore blocks in a recursive fashion as per #420.
WyCS: Added test cases for #423.

These test that a contradiction is determined for when x is a strict
subset of y and vice versa.
WyCS: Partial fix for #423.

This fixes the discrepency between the use of case blocks and inline
logical OR expressions.  However, it doesn't fix the underlying problem
that these test cases should pass.
WyCS: Added more test cases for #423.

I thought of a few more useful test cases which relate to #423.
Currently they are not passing, though ideally they would be.  There
appears to be a missing rule in the verifier for this case.
WyCS: Added Solver Rule for #423.

This rule handles the case where x contains y and y contains x, so x ==
y.
WyC: Minor tweak for consistent error reporting.

In adding the assert block, the way that failing assertions were
reported was different, and this was causing the regression tests to
fail.