Merge

6 files changed, 111 insertions, 95 deletions

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index f38e0093..78774876 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -39,7 +39,6 @@ var $Heap: HeapType;
 

 var $Alloc: [Ref] bool;

 procedure {:inline 1} Alloc() returns (x: Ref)

-  free ensures x != null;

   modifies $Alloc;

 {

   assume $Alloc[x] == false && x != null;

@@ -57,6 +56,11 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
 axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

 axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

 

+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

+{

+  $result := $TypeOf($DynamicType(this));

+}

+

 ";

     private Sink sink;

 

@@ -83,6 +87,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
     public override Bpl.Variable CreateFieldVariable(IFieldReference field) {

       Bpl.Variable v;

       string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;

+      fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);

       Bpl.IToken tok = field.Token();

       Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);

 

@@ -101,6 +106,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
     public override Bpl.Variable CreateEventVariable(IEventDefinition e) {

       Bpl.Variable v;

       string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;

+      eventName = TranslationHelper.TurnStringIntoValidIdentifier(eventName);

       Bpl.IToken tok = e.Token();

       Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType);

 

@@ -109,7 +115,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
         v = new Bpl.GlobalVariable(tok, tident);

       }

       else {

-        Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);

+        Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.RefType), t);

         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, mt);

         v = new Bpl.GlobalVariable(tok, tident);

       }

@@ -126,11 +132,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
     /// </param>

     public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType) {

       if (accessType == AccessType.Struct)

-        return Bpl.Expr.Select(o, f);

+        return Unbox(f.tok, unboxType, Bpl.Expr.Select(o, f));

       else if (accessType == AccessType.Heap)

         return Bpl.Expr.Select(f, o);

       else

-        return Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f);

+        return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));

     }

 

     /// <summary>

@@ -140,11 +146,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
     public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType) {

       Debug.Assert(o != null);

       if (accessType == AccessType.Struct)

-        return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, value);

+        return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, Box(f.tok, boxType, value));

       else if (accessType == AccessType.Heap)

         return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)f, o, value);

       else

-        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, value)));

+        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value))));

     }

 

   }

@@ -176,7 +182,6 @@ type HeapType = [Ref,Field]Box;
 

 var $Alloc: [Ref] bool;

 procedure {:inline 1} Alloc() returns (x: Ref)

-  free ensures x != null;

   modifies $Alloc;

 {

   assume $Alloc[x] == false && x != null;

@@ -194,6 +199,11 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
 axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

 axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

 

+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

+{

+  $result := $TypeOf($DynamicType(this));

+}

+

 ";

     private Sink sink;

 

@@ -241,6 +251,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
     public override Bpl.Variable CreateEventVariable(IEventDefinition e) {

       Bpl.Variable v;

       string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;

+      fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);

       Bpl.IToken tok = e.Token();

 

       if (e.Adder.ResolvedMethod.IsStatic) {

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 646b16f1..a358e3c0 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -20,14 +20,14 @@ const null: ref;
 

 type Set T = [T]bool;

 

-function Set#Empty<T>() returns (Set T);

+function Set#Empty<T>(): Set T;

 axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

 

-function Set#Singleton<T>(T) returns (Set T);

+function Set#Singleton<T>(T): Set T;

 axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

 axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

 

-function Set#UnionOne<T>(Set T, T) returns (Set T);

+function Set#UnionOne<T>(Set T, T): Set T;

 axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }

   Set#UnionOne(a,x)[o] <==> o == x || a[o]);

 axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }

@@ -35,7 +35,7 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
 axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }

   a[y] ==> Set#UnionOne(a, x)[y]);

 

-function Set#Union<T>(Set T, Set T) returns (Set T);

+function Set#Union<T>(Set T, Set T): Set T;

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }

   Set#Union(a,b)[o] <==> a[o] || b[o]);

 axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }

@@ -47,7 +47,7 @@ axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
     Set#Difference(Set#Union(a, b), a) == b &&

     Set#Difference(Set#Union(a, b), b) == a);

 

-function Set#Intersection<T>(Set T, Set T) returns (Set T);

+function Set#Intersection<T>(Set T, Set T): Set T;

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

   Set#Intersection(a,b)[o] <==> a[o] && b[o]);

 

@@ -60,27 +60,27 @@ axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }
 axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }

   Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

 

-function Set#Difference<T>(Set T, Set T) returns (Set T);

+function Set#Difference<T>(Set T, Set T): Set T;

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

   Set#Difference(a,b)[o] <==> a[o] && !b[o]);

 axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }

   b[y] ==> !Set#Difference(a, b)[y] );

 

-function Set#Subset<T>(Set T, Set T) returns (bool);

+function Set#Subset<T>(Set T, Set T): bool;

 axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }

   Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));

 

-function Set#Equal<T>(Set T, Set T) returns (bool);

+function Set#Equal<T>(Set T, Set T): bool;

 axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }

   Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));

 axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }  // extensionality axiom for sets

   Set#Equal(a,b) ==> a == b);

 

-function Set#Disjoint<T>(Set T, Set T) returns (bool);

+function Set#Disjoint<T>(Set T, Set T): bool;

 axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }

   Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));

 

-function Set#Choose<T>(Set T, TickType) returns (T);

+function Set#Choose<T>(Set T, TickType): T;

 axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }

   a != Set#Empty() ==> a[Set#Choose(a, tick)]);

 

@@ -90,25 +90,25 @@ axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
 

 type Seq T;

 

-function Seq#Length<T>(Seq T) returns (int);

+function Seq#Length<T>(Seq T): int;

 axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

 

-function Seq#Empty<T>() returns (Seq T);

+function Seq#Empty<T>(): Seq T;

 axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);

 axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

 

-function Seq#Singleton<T>(T) returns (Seq T);

+function Seq#Singleton<T>(T): Seq T;

 axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);

 

-function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);

+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int): Seq T;

 axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }

   0 <= len ==> Seq#Length(Seq#Build(s,i,v,len)) == len);

 

-function Seq#Append<T>(Seq T, Seq T) returns (Seq T);

+function Seq#Append<T>(Seq T, Seq T): Seq T;

 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }

   Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));

 

-function Seq#Index<T>(Seq T, int) returns (T);

+function Seq#Index<T>(Seq T, int): T;

 axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);

 axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }

   (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&

@@ -118,7 +118,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Bui
     (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&

     (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));

 

-function Seq#Update<T>(Seq T, int, T) returns (Seq T);

+function Seq#Update<T>(Seq T, int, T): Seq T;

 axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }

   0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));

 axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }

@@ -126,7 +126,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v)
     (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&

     (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));

 

-function Seq#Contains<T>(Seq T, T) returns (bool);

+function Seq#Contains<T>(Seq T, T): bool;

 axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }

   Seq#Contains(s,x) <==>

     (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));

@@ -153,22 +153,22 @@ axiom (forall<T> s: Seq T, n: int, x: T ::
     (exists i: int :: { Seq#Index(s, i) }

       0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

 

-function Seq#Equal<T>(Seq T, Seq T) returns (bool);

+function Seq#Equal<T>(Seq T, Seq T): bool;

 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }

   Seq#Equal(s0,s1) <==>

     Seq#Length(s0) == Seq#Length(s1) &&

     (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

         0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

-axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences

+axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences

   Seq#Equal(a,b) ==> a == b);

 

-function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);

+function Seq#SameUntil<T>(Seq T, Seq T, int): bool;

 axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }

   Seq#SameUntil(s0,s1,n) <==>

     (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

         0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

 

-function Seq#Take<T>(s: Seq T, howMany: int) returns (Seq T);

+function Seq#Take<T>(s: Seq T, howMany: int): Seq T;

 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }

   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

@@ -177,7 +177,7 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:w
   0 <= j && j < n && j < Seq#Length(s) ==>

     Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

 

-function Seq#Drop<T>(s: Seq T, howMany: int) returns (Seq T);

+function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;

 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }

   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

@@ -197,8 +197,8 @@ axiom (forall<T> s, t: Seq T ::
 

 type BoxType;

 

-function $Box<T>(T) returns (BoxType);

-function $Unbox<T>(BoxType) returns (T);

+function $Box<T>(T): BoxType;

+function $Unbox<T>(BoxType): T;

 

 axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

 axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);

@@ -206,7 +206,10 @@ axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
 axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);

 axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);

 axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);

-// note: an axiom like this for bool would not be sound

+// Note: an axiom like this for bool would not be sound; instead, we do:

+function $IsCanonicalBoolBox(BoxType): bool;

+axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));

+axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);

 

 // ---------------------------------------------------------------

 // -- Encoding of type names -------------------------------------

@@ -218,12 +221,12 @@ const unique class.bool: ClassName;
 const unique class.set: ClassName;

 const unique class.seq: ClassName;

 

-function /*{:never_pattern true}*/ dtype(ref) returns (ClassName);

-function /*{:never_pattern true}*/ TypeParams(ref, int) returns (ClassName);

+function /*{:never_pattern true}*/ dtype(ref): ClassName;

+function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;

 

-function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);

-function TypeTupleCar(ClassName) returns (ClassName);

-function TypeTupleCdr(ClassName) returns (ClassName);

+function TypeTuple(a: ClassName, b: ClassName): ClassName;

+function TypeTupleCar(ClassName): ClassName;

+function TypeTupleCdr(ClassName): ClassName;

 // TypeTuple is injective in both arguments:

 axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }

   TypeTupleCar(TypeTuple(a,b)) == a &&

@@ -235,13 +238,13 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type DatatypeType;

 

-function /*{:never_pattern true}*/ DtType(DatatypeType) returns (ClassName);  // the analog of dtype for datatype values

-function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int) returns (ClassName);  // the analog of TypeParams

+function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName;  // the analog of dtype for datatype values

+function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName;  // the analog of TypeParams

 

 type DtCtorId;

-function DatatypeCtorId(DatatypeType) returns (DtCtorId);

+function DatatypeCtorId(DatatypeType): DtCtorId;

 

-function DtRank(DatatypeType) returns (int);

+function DtRank(DatatypeType): int;

 

 // ---------------------------------------------------------------

 // -- Axiom contexts ---------------------------------------------

@@ -274,7 +277,7 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
   MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);

 

 

-function DeclType<T>(Field T) returns (ClassName);

+function DeclType<T>(Field T): ClassName;

 

 // ---------------------------------------------------------------

 // -- Allocatedness ----------------------------------------------

@@ -339,10 +342,10 @@ type HeapType = <alpha>[ref,Field alpha]alpha;
 function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }

 function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }

 

-function $IsGoodHeap(HeapType) returns (bool);

+function $IsGoodHeap(HeapType): bool;

 var $Heap: HeapType where $IsGoodHeap($Heap);

 

-function $HeapSucc(HeapType, HeapType) returns (bool);

+function $HeapSucc(HeapType, HeapType): bool;

 axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }

   $HeapSucc(h, update(h, r, f, x)));

 axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 253a1f9b..67559aee 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3676,11 +3676,15 @@ namespace Microsoft.Dafny {
         Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);

         Bpl.Expr unbox = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI);

 

+        Bpl.Expr c = GetBoolBoxCondition(xSubI, st.Arg);

         Bpl.Expr wh = GetWhereClause(tok, unbox, st.Arg, etran);

         if (wh != null) {

+          c = BplAnd(c, wh);

+        }

+        if (c != Bpl.Expr.True) {

           Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);

           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));

-          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, wh));

+          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, c));

         }

 

       } else if (type.IsRefType) {

@@ -3706,6 +3710,18 @@ namespace Microsoft.Dafny {
       return null;

     }

 

+    Bpl.Expr GetBoolBoxCondition(Expr box, Type type) {

+      Contract.Requires(box != null);

+      Contract.Requires(type != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      if (type is BoolType) {

+        return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box);

+      } else {

+        return Bpl.Expr.True;

+      }

+    }

+

     void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals,

                       ExpressionTranslator etran)

     {

@@ -4826,6 +4842,7 @@ namespace Microsoft.Dafny {
       

       Box,

       Unbox,

+      IsCanonicalBoolBox,

       

       IsGoodHeap,

       HeapSucc,

@@ -4957,6 +4974,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

           return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);

+        case BuiltinFunction.IsCanonicalBoolBox:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$IsCanonicalBoolBox", Bpl.Type.Bool, args);

 

         case BuiltinFunction.IsGoodHeap:

           Contract.Assert(args.Length == 1);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 070aa6be..2463b0e5 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -209,7 +209,7 @@ Execution trace:
     (0,0): anon15

     (0,0): anon25_Else

 

-Dafny program verifier finished with 39 verified, 14 errors

+Dafny program verifier finished with 41 verified, 14 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ef2049a3..a5f02dc6 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -308,3 +308,13 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
     assert x == y;

   }

 }

+

+// ----------------------- tests that involve sequences of boxed booleans --------

+

+ghost method M(zeros: seq<bool>, Z: bool)

+  requires 1 <= |zeros| && Z == false;

+  requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;

+{

+  var x := [Z];

+  assert zeros[0..1] == [Z];

+}

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index b837237b..c0185e9c 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,50 +1,23 @@
-# Aste started: 2011-05-14 07:00:16

+# Aste started: 2011-05-17 07:00:09

 # Host id: Boogiebox

-# [2011-05-14 07:02:49] SpecSharp revision: 5fb7af71cc82

-# [2011-05-14 07:02:49] SscBoogie revision: 5fb7af71cc82

-# [2011-05-14 07:04:08] Boogie revision: 76b4d17abc74

-[2011-05-14 07:06:08] [Error] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+# [2011-05-17 07:02:41] SpecSharp revision: 5fb7af71cc82

+# [2011-05-17 07:02:41] SscBoogie revision: 5fb7af71cc82

+# [2011-05-17 07:03:56] Boogie revision: e6ac2aed917f

+[2011-05-17 07:06:14] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected


-    D:\Temp\aste\Boogie\Source\Core\ResolutionContext.cs(173,7): error CC1016: Contract.Assert/Contract.Assume cannot be used in contract section. Use only Requires and Ensures.


     D:\Temp\aste\Boogie\Source\Core\Absy.cs(682,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(109,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(114,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(117,65): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.


-    C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(215,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite" /level:4 /rewrite  "/assemblyMode=standard" /throwonfailure /libpaths:"D:\Temp\aste\Boogie\Source\AIFramework\bin\Checked\;D:\Temp\aste\Boogie\Source\Basetypes\bin\Checked\;D:\Temp\aste\Boogie\Source\CodeContractsExtender\bin\Checked\;D:\Temp\aste\Boogie\Source\Graph\bin\Checked\;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.0\Profile\Client\;D:\Temp\aste\Boogie\Source\ParserHelper\bin\Checked\;D:\Temp\aste\Boogie\Source\AIFramework\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\Basetypes\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\CodeContractsExtender\bin\Checked\CodeContracts;D:\Temp\aste\Boogie\Source\Graph\bin\Checked\CodeContracts;C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.0\Profile\Client\CodeContracts;D:\Temp\aste\Boogie\Source\ParserHelper\bin\Checked\CodeContracts;C:\Program Files (x86)\Microsoft\Contracts\Contracts\.NETFramework\v4.0 " "Core.dll"" exited with code 1.


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCExpr\bin\Checked\VCExpr.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\VCGeneration\bin\Checked\VCGeneration.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Z3\bin\Checked\Provers.Z3.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\TPTP\bin\Checked\Provers.TPTP.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Isabelle\bin\Checked\Provers.Isabelle.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\Simplify\bin\Checked\Provers.Simplify.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\bin\Checked\Provers.SMTLib.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\AbsInt\bin\Checked\AbsInt.dll' could not be found


-    error CS0006: Metadata file 'D:\Temp\aste\Boogie\Source\Core\bin\Checked\Core.dll' could not be found


+    D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(111,7): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(290,7): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(309,7): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1662,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1822,11): warning CS0162: Unreachable code detected


+    D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(662,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0162: Unreachable code detected


@@ -52,13 +25,11 @@
     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.ComputeFreeVariables(Microsoft.Boogie.Set)' overrides 'Microsoft.Boogie.Expr.ComputeFreeVariables(Microsoft.Boogie.Set)', thus cannot add Requires.


-    1 error

-    1 error

-    2 error

-    3 error

-    3 error

-    4 error

-    4 error

-    5 error

-    8 error

-    10 failed

+    warning CS0162: Unreachable code detected


+    warning CS0162: Unreachable code detected


+    warning CS0162: Unreachable code detected


+    warning CS0162: Unreachable code detected


+    warning CS0162: Unreachable code detected


+    warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


+[2011-05-17 07:54:06] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2011-05-17 07:55:08] Released nightly of Boogie