Add mising if test for BitVectorType

closes #39
dafny-lang · Oct 6, 2016 · 3f899b9 · 3f899b9
1 parent cad9ce6
commit 3f899b9
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 0 deletions.
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
@@ -10147,6 +10147,8 @@ bool CompatibleDecreasesTypes(Type t, Type u) {
         return u is MapType && ((MapType)t).Finite == ((MapType)u).Finite;
       } else if (t is ArrowType) {
         return u is ArrowType;
+      } else if (t is BitvectorType) {
+        return u is BitvectorType;
       } else {
         Contract.Assert(t.IsTypeParameter || t.IsInternalTypeSynonym);
         return false;  // don't consider any type parameters to be the same (since we have no comparison function for them anyway)
@@ -10263,6 +10265,12 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
         less = Bpl.Expr.False;
         atmost = Bpl.Expr.False;
 
+      } else if (ty0 is BitvectorType) {
+        BitvectorType bv = (BitvectorType)ty0;
+        eq = Bpl.Expr.Eq(e0, e1);
+        less = FunctionCall(tok, "lt_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
+        atmost = FunctionCall(tok, "ge_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
+
       } else {
         // reference type
         Contract.Assert(ty0.IsRefType);  // otherwise, unexpected type

diff --git a/Test/dafny4/git-issue39.dfy b/Test/dafny4/git-issue39.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function BitsAsInt(b:bv32): int
+    ensures 0 <= BitsAsInt(b) < 0x1_0000_0000
+{
+    b as int
+}
diff --git a/Test/dafny4/git-issue39.dfy.expect b/Test/dafny4/git-issue39.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@

		Dafny program verifier finished with 1 verified, 0 errors