Fix #148

This puts through fixes for casts.  Everything is getting a bit ugly it would
seem, but that's life :)

src/main/java/wyboogie/tasks/BoogieCompiler.java

@@ -1657,7 +1657,12 @@ public Expr constructBitwiseShiftRight(WyilFile.Expr.BitwiseShiftRight expr, Exp
 
     @Override
     public Expr constructCast(WyilFile.Expr.Cast expr, Expr operand) {
-        return cast(expr.getType(), expr.getOperand().getType(), operand);
+        Expr e = cast(expr.getType(), expr.getOperand().getType(), operand);
+		// TODO: this is a bit of a kludge. The generate cast uses attributes from the
+		// operand, where as we want to have the attribute refer to the cast itself. A
+		// better solution would be to add an extra argument to cast.
+        e.getAttributes()[0] = ATTRIBUTE(expr);
+        return e;
     }
 
     @Override
@@ -3182,7 +3187,7 @@ private List<Expr.Logical> constructTypeConstraints(Tuple<WyilFile.Decl.Variable
      * @param argument The argument being tested.
      * @return
      */
-    private Expr.Logical constructTypeTest(WyilFile.Type to, WyilFile.Type from, Expr argument, Expr heap, Syntactic.Item item) {
+    public Expr.Logical constructTypeTest(WyilFile.Type to, WyilFile.Type from, Expr argument, Expr heap, Syntactic.Item item) {
         switch (to.getOpcode()) {
             case WyilFile.TYPE_any:
                 return NEQ(box(from, argument), VOID, ATTRIBUTE(item));
@@ -3228,7 +3233,7 @@ private Expr.Logical constructTypeTest(WyilFile.Type to, WyilFile.Type from, Exp
      * @param item
      * @return
      */
-    private Expr.Logical constructTypeTest(WyilFile.Type type, Expr argument, Expr heap, Syntactic.Item item) {
+    public Expr.Logical constructTypeTest(WyilFile.Type type, Expr argument, Expr heap, Syntactic.Item item) {
          switch (type.getOpcode()) {
              case WyilFile.TYPE_bool:
              case WyilFile.TYPE_byte:
@@ -4428,7 +4433,7 @@ private String get(String lab) {
     /**
      * The name used to represent the heap variable which is passed into a method.
      */
-    private static Expr.VariableAccess HEAP = VAR("HEAP");
+    public static Expr.VariableAccess HEAP = VAR("HEAP");
     private static Expr.VariableAccess OHEAP = VAR("#HEAP");
     private static Expr OLD_HEAP = OLD(HEAP);
     private static Decl.Variable HEAP_PARAM = new Decl.Variable("HEAP",REFMAP);

src/main/java/wyboogie/util/DefinednessExtractor.java

@@ -197,11 +197,18 @@ public List<Stmt.Assert> constructRemainder(Expr.Remainder expr, List<Stmt.Asser
 
     @Override
     public List<Stmt.Assert> constructInvoke(Expr.Invoke expr, List<List<Stmt.Assert>> preconditions) {
+        Syntactic.Item wyItem = expr.getAttribute(Syntactic.Item.class);
         List<Stmt.Assert> rs = flattern(preconditions, l -> l);
         // Special case!
         if (expr.getName().equals("Array#Generator")) {
             Expr len = expr.getArguments().get(1);
             rs.add(ASSERT(LTEQ(CONST(0), len, len.getAttributes()), ATTRIBUTE(WyilFile.STATIC_NEGATIVE_LENGTH_FAILURE)));
+        } else if(wyItem instanceof WyilFile.Expr.Cast) {
+        	WyilFile.Expr.Cast c = (WyilFile.Expr.Cast) wyItem;
+        	Expr arg = bc.reconstructExpression(c.getOperand());
+        	//Expr arg = expr.getArguments().get(0);
+        	Expr.Logical test = bc.constructTypeTest(c.getType(), c.getOperand().getType(), arg, BoogieCompiler.HEAP, wyItem);
+        	rs.add(ASSERT(test, ATTRIBUTE(WyilFile.STATIC_TYPEINVARIANT_FAILURE)));
         }
         return rs;
     }

src/test/java/wyboogie/WhileyCompilerTests.java

@@ -112,7 +112,7 @@ public void debugTests(Trie path) throws IOException {
 
 	// Here we enumerate all available test cases.
 	private static Stream<Trie> debugFiles() throws IOException {
-		return readTestFiles(WHILEY_SRC_DIR, in(190,1163,1164,1418));
+		return readTestFiles(WHILEY_SRC_DIR, in(125,809));
 //		return readTestFiles(WHILEY_SRC_DIR, atleast(99999));
 	}
 

tests/000920.test

@@ -16,4 +16,4 @@ public export method test():
        assume f() == 0
 ---
 E702 main.whiley 9,11:19
-E717 main.whiley 9,4:19
+E718 main.whiley 9,11:19

tests/001250.test

@@ -18,4 +18,4 @@ public export method test():
     f((pos) 1)
 ---
 E702 main.whiley 10,10:16
-E716 main.whiley 10,8:17
+E718 main.whiley 10,10:16

tests/001269.test

@@ -15,4 +15,4 @@ public export method test():
     g(-1)
 ---
 E702 main.whiley 7,11:17
-E717 main.whiley 7,4:17
+E718 main.whiley 7,11:17

tests/001292.test

@@ -17,4 +17,4 @@ public export method test():
    assume g(0) == 0
 ---
 E702 main.whiley 9,13:23
-E716 main.whiley 9,11:24
+E718 main.whiley 9,13:23

tests/001293.test

@@ -22,4 +22,4 @@ public export method test():
    assume f(0) == 0
 ---
 E702 main.whiley 14,11:20
-E717 main.whiley 14,4:20
+E718 main.whiley 14,11:20