Merge

22 files changed, 471 insertions, 104 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 09b6efcf..742fd4e4 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -371,6 +371,15 @@ axiom (forall<U, V> u: U ::
   { Map#Domain(Map#Empty(): Map U V)[u] }

    !Map#Domain(Map#Empty(): Map U V)[u]);

 

+function Map#Glue<U, V>([U] bool, [U]V): Map U V;

+axiom (forall<U, V> a: [U] bool, b:[U]V ::

+  { Map#Domain(Map#Glue(a, b)) }

+    Map#Domain(Map#Glue(a, b)) == a);

+axiom (forall<U, V> a: [U] bool, b:[U]V ::

+  { Map#Elements(Map#Glue(a, b)) }

+    Map#Elements(Map#Glue(a, b)) == b);

+

+

 //Build is used in displays, and for map updates

 function Map#Build<U, V>(Map U V, U, V): Map U V;

 /*axiom (forall<U, V> m: Map U V, u: U, v: V ::

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 67669245..f7eecfc5 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -274,6 +274,19 @@ namespace Dafny
       }

       return new MultiSet<T>(r);

     }

+    public IEnumerable<T> Elements {

+      get {

+        List<T> l = new List<T>();

+        foreach (T t in dict.Keys) {

+          int n;

+          dict.TryGetValue(t, out n);

+          for (int i = 0; i < n; i ++) {

+            l.Add(t);

+          }

+        }

+        return l;

+      }

+    }

   }

 

   public class Map<U, V>

@@ -288,9 +301,16 @@ namespace Dafny
         return new Map<U, V>(new Dictionary<U,V>());

       }

     }

-    public static Map<U, V> FromElements(params Pair<U,V>[] values) {

+    public static Map<U, V> FromElements(params Pair<U, V>[] values) {

       Dictionary<U, V> d = new Dictionary<U, V>(values.Length);

-      foreach (Pair<U,V> p in values) {

+      foreach (Pair<U, V> p in values) {

+        d[p.Car] = p.Cdr;

+      }

+      return new Map<U, V>(d);

+    }

+    public static Map<U, V> FromCollection(List<Pair<U, V>> values) {

+      Dictionary<U, V> d = new Dictionary<U, V>(values.Count);

+      foreach (Pair<U, V> p in values) {

         d[p.Car] = p.Cdr;

       }

       return new Map<U, V>(d);

@@ -343,6 +363,11 @@ namespace Dafny
       d[index] = val;

       return new Map<U, V>(d);

     }

+    public IEnumerable<U> Domain {

+      get {

+        return dict.Keys;

+      }

+    }

   }

   public class Sequence<T>

   {

@@ -471,6 +496,12 @@ namespace Dafny
       }

       return frall;

     }

+    public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {

+      foreach (var u in map.Domain) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

     public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {

       foreach (var u in seq.Elements) {

         if (pred(u) != frall) { return !frall; }

@@ -479,6 +510,7 @@ namespace Dafny
     }

     // Enumerating other collections

     public delegate Dafny.Set<T> ComprehensionDelegate<T>();

+    public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();

     public static IEnumerable<bool> AllBooleans {

       get {

         yield return false;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d7fcca7a..148a739d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -590,7 +590,25 @@ namespace Microsoft.Boogie {
                     if (!found) {

                         Block auxNewBlock = new Block();

                         auxNewBlock.Label = ((Block)bl).Label;

-                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds);

+                        auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);

+                        //add restoration code for such blocks

+                        if (loopHeaderToAssignCmd.ContainsKey(header))

+                        {

+                            AssignCmd assignCmd = loopHeaderToAssignCmd[header];

+                            auxNewBlock.Cmds.Add(assignCmd);

+                        }

+                        List<AssignLhs> lhsg = new List<AssignLhs>();

+                        IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

+                        foreach (IdentifierExpr gl in globalsMods)

+                            lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));

+                        List<Expr> rhsg = new List<Expr>();

+                        foreach (IdentifierExpr gl in globalsMods)

+                            rhsg.Add(new OldExpr(Token.NoToken, gl));

+                        if (lhsg.Count != 0)

+                        {

+                            AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);

+                            auxNewBlock.Cmds.Add(globalAssignCmd);

+                        }

                         blockMap[(Block)bl] = auxNewBlock;

                     }

                 }

@@ -666,21 +684,6 @@ namespace Microsoft.Boogie {
             if (newTargets.Length == 0) {

                 if (!detLoopExtract)

                     newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

-                else {

-                    if (loopHeaderToAssignCmd.ContainsKey(header)) {

-                        AssignCmd assignCmd = loopHeaderToAssignCmd[header];

-                        newBlock.Cmds.Add(assignCmd);

-                    }

-                    List<AssignLhs> lhsg = new List<AssignLhs>();

-                    IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;

-                    foreach (IdentifierExpr gl in globalsMods)

-                        lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));

-                    List<Expr> rhsg = new List<Expr>();

-                    foreach (IdentifierExpr gl in globalsMods)

-                        rhsg.Add(new OldExpr(Token.NoToken, gl));

-                    AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);

-                    newBlock.Cmds.Add(globalAssignCmd);

-                }

                 newBlock.TransferCmd = new ReturnCmd(Token.NoToken);

             } else {

               newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5baf8667..c28d8c8a 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1222,7 +1222,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

-              ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)

+              ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

+              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 71f7bbb4..63103399 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -384,7 +384,7 @@ namespace Microsoft.Boogie {
       codeCopier.OldSubst = null;

     }

 

-    private Cmd InlinedRequires(Implementation impl, CallCmd callCmd, Requires req) {

+    private Cmd InlinedRequires(CallCmd callCmd, Requires req) {

       Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

       if (req.Free)

         reqCopy.Condition = Expr.True;

@@ -395,15 +395,16 @@ namespace Microsoft.Boogie {
       return a;

     }

 

-    private Cmd InlinedEnsures(Implementation impl, CallCmd callCmd, Ensures ens) {

-      if (impl.FindExprAttribute("inline") != null && !ens.Free) {

+    private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {

+      if (QKeyValue.FindBoolAttribute(ens.Attributes, "assume")) {

+        return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

+      } else if (ens.Free) {

+        return new AssumeCmd(ens.tok, Expr.True); 

+      } else {

         Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());

         ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);

         return new AssertEnsuresCmd(ensCopy);

       }

-      else {

-        return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));

-      }

     }

 

     private CmdSeq RemoveAsserts(CmdSeq cmds) {

@@ -448,7 +449,7 @@ namespace Microsoft.Boogie {
       // inject requires

       for (int i = 0; i < proc.Requires.Length; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

-        inCmds.Add(InlinedRequires(impl, callCmd, req));

+        inCmds.Add(InlinedRequires(callCmd, req));

       }

 

       VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);

@@ -509,7 +510,7 @@ namespace Microsoft.Boogie {
       // inject ensures

       for (int i = 0; i < proc.Ensures.Length; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

-        outCmds.Add(InlinedEnsures(impl, callCmd, ens));

+        outCmds.Add(InlinedEnsures(callCmd, ens));

       }

 

       // assign out params

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 232224b0..fad4e7fa 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1990,6 +1990,11 @@ namespace Microsoft.Dafny {
             wr.Write("Dafny.Helpers.QuantSet(");

             TrExpr(b.Set);

             wr.Write(", ");

+          } else if (bound is QuantifierExpr.MapBoundedPool) {

+            var b = (QuantifierExpr.MapBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantMap(");

+            TrExpr(b.Map);

+            wr.Write(", ");

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSeq(");

@@ -2047,6 +2052,11 @@ namespace Microsoft.Dafny {
             wr.Write("foreach (var @{0} in (", bv.Name);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

+          } else if (bound is QuantifierExpr.MapBoundedPool) {

+            var b = (QuantifierExpr.MapBoundedPool)bound;

+            wr.Write("foreach (var @{0} in (", bv.Name);

+            TrExpr(b.Map);

+            wr.Write(").Domain) { ");

           } else if (bound is QuantifierExpr.SeqBoundedPool) {

             var b = (QuantifierExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.Name);

@@ -2067,6 +2077,70 @@ namespace Microsoft.Dafny {
         wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);

         wr.Write("})()");

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        // For "map i | R(i) :: Term(i)" where the term has type "V" and i has type "U", emit something like:

+        // ((MapComprehensionDelegate<U, V>)delegate() {

+        //   var _coll = new List<Pair<U,V>>();

+        //   foreach (L l in sq.Elements) {

+        //     foreach (K k in st.Elements) {

+        //       for (BigInteger j = Lo; j < Hi; j++) {

+        //         for (bool i in Helper.AllBooleans) {

+        //           if (R(i,j,k,l)) {

+        //             _coll.Add(new Pair(i, Term(i));

+        //           }

+        //         }

+        //       }

+        //     }

+        //   }

+        //   return Dafny.Map<U, V>.FromElements(_coll);

+        // })()

+        Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

+        var domtypeName = TypeName(((MapType)e.Type).Domain);

+        var rantypeName = TypeName(((MapType)e.Type).Range);

+        wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);

+        wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);

+        var n = e.BoundVars.Count;

+        Contract.Assert(e.Bounds.Count == n && n == 1);

+        var bound = e.Bounds[0];

+        var bv = e.BoundVars[0];

+        if (bound is QuantifierExpr.BoolBoundedPool) {

+          wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.Name);

+        } else if (bound is QuantifierExpr.IntBoundedPool) {

+          var b = (QuantifierExpr.IntBoundedPool)bound;

+          wr.Write("for (var @{0} = ", bv.Name);

+          TrExpr(b.LowerBound);

+          wr.Write("; @{0} < ", bv.Name);

+          TrExpr(b.UpperBound);

+          wr.Write("; @{0}++) {{ ", bv.Name);

+        } else if (bound is QuantifierExpr.SetBoundedPool) {

+          var b = (QuantifierExpr.SetBoundedPool)bound;

+          wr.Write("foreach (var @{0} in (", bv.Name);

+          TrExpr(b.Set);

+          wr.Write(").Elements) { ");

+        } else if (bound is QuantifierExpr.MapBoundedPool) {

+          var b = (QuantifierExpr.MapBoundedPool)bound;

+          wr.Write("foreach (var @{0} in (", bv.Name);

+          TrExpr(b.Map);

+          wr.Write(").Domain) { ");

+        } else if (bound is QuantifierExpr.SeqBoundedPool) {

+          var b = (QuantifierExpr.SeqBoundedPool)bound;

+          wr.Write("foreach (var @{0} in (", bv.Name);

+          TrExpr(b.Seq);

+          wr.Write(").Elements) { ");

+        } else {

+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

+        }

+        wr.Write("if (");

+        TrExpr(e.Range);

+        wr.Write(") { ");

+        wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.Name);

+        TrExpr(e.Term);

+        wr.Write(")); }");

+        wr.Write("}");

+        wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName);

+        wr.Write("})()");

+

       } else if (expr is PredicateExpr) {

         var e = (PredicateExpr)expr;

         TrExpr(e.Body);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 103cb5c7..97da97e3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1342,14 +1342,28 @@ MultiSetExpr<out Expression e>
   .

 MapExpr<out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-     IToken/*!*/ x = null;  List<ExpressionPair/*!*/>/*!*/ elements;

+     IToken/*!*/ x = Token.NoToken;

+     List<ExpressionPair/*!*/>/*!*/ elements;

      e = dummyExpr;

   .)

   "map"                                        (. x = t; .)

-  ( "{"                                        (. elements = new List<ExpressionPair/*!*/>(); .)

+  ( "["                                        (. elements = new List<ExpressionPair/*!*/>(); .)

       [ MapLiteralExpressions<out elements> ]  (. e = new MapDisplayExpr(x, elements);.)

-    "}"

-  | (. SemErr("map must be followed by braces."); .)

+    "]"

+  | (

+     (. 

+     BoundVar/*!*/ bv;

+     List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+     Expression/*!*/ range;

+     Expression body = null;

+    .)

+      IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

+      "|" Expression<out range>

+      QSep

+      Expression<out body>

+      (. e = new MapComprehension(x, bvars, range, body); .) 

+    )

+  | (. SemErr("map must be followed by literal in brackets or comprehension."); .)

   )

   .

 MapLiteralExpressions<.out List<ExpressionPair> elements.>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b42fcb5a..5fd34e65 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -577,7 +577,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for:

-  ///     set(Arg) or seq(Arg)

+  ///     set(Arg) or seq(Arg) or map(Arg, Range)

   /// </summary>

   public class CollectionTypeProxy : RestrictedTypeProxy {

     public readonly Type Arg;

@@ -3068,6 +3068,11 @@ namespace Microsoft.Dafny {
       public readonly Expression Set;

       public SetBoundedPool(Expression set) { Set = set; }

     }

+    public class MapBoundedPool : BoundedPool

+    {

+      public readonly Expression Map;

+      public MapBoundedPool(Expression map) { Map = map; }

+    }

     public class SeqBoundedPool : BoundedPool

     {

       public readonly Expression Seq;

@@ -3162,6 +3167,17 @@ namespace Microsoft.Dafny {
       TermIsImplicit = term == null;

     }

   }

+  public class MapComprehension : ComprehensionExpr

+  {

+    public MapComprehension(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ range, Expression term)

+      : base(tok, bvars, range, term, null) {

+      Contract.Requires(tok != null);

+      Contract.Requires(cce.NonNullElements(bvars));

+      Contract.Requires(1 <= bvars.Count);

+      Contract.Requires(range != null);

+      Contract.Requires(term != null);

+    }

+  }

 

   public class WildcardExpr : Expression

   {  // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 817df12b..fe4d58a9 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2303,21 +2303,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void MapExpr(out Expression e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-		IToken/*!*/ x = null;  List<ExpressionPair/*!*/>/*!*/ elements;

+		IToken/*!*/ x = Token.NoToken;

+		List<ExpressionPair/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

 		Expect(42);

 		x = t; 

-		if (la.kind == 6) {

+		if (la.kind == 55) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(9)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(7);

+			Expect(56);

+		} else if (la.kind == 1) {

+			BoundVar/*!*/ bv;

+			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+			Expression/*!*/ range;

+			Expression body = null;

+			

+			IdentTypeOptional(out bv);

+			bvars.Add(bv); 

+			Expect(18);

+			Expression(out range);

+			QSep();

+			Expression(out body);

+			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

-			SemErr("map must be followed by braces."); 

+			SemErr("map must be followed by literal in brackets or comprehension."); 

 		} else SynErr(177);

 	}

 

@@ -2426,6 +2440,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

+	void QSep() {

+		if (la.kind == 106) {

+			Get();

+		} else if (la.kind == 107) {

+			Get();

+		} else SynErr(179);

+	}

+

 	void MatchExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

@@ -2454,7 +2476,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 104 || la.kind == 105) {

 			Exists();

 			x = t; 

-		} else SynErr(179);

+		} else SynErr(180);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2524,7 +2546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 103) {

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void Exists() {

@@ -2532,14 +2554,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 105) {

 			Get();

-		} else SynErr(181);

-	}

-

-	void QSep() {

-		if (la.kind == 106) {

-			Get();

-		} else if (la.kind == 107) {

-			Get();

 		} else SynErr(182);

 	}

 

@@ -2800,10 +2814,10 @@ public class Errors {
 			case 176: s = "invalid MultiSetExpr"; break;

 			case 177: s = "invalid MapExpr"; break;

 			case 178: s = "invalid ConstAtomExpression"; break;

-			case 179: s = "invalid QuantifierGuts"; break;

-			case 180: s = "invalid Forall"; break;

-			case 181: s = "invalid Exists"; break;

-			case 182: s = "invalid QSep"; break;

+			case 179: s = "invalid QSep"; break;

+			case 180: s = "invalid QuantifierGuts"; break;

+			case 181: s = "invalid Forall"; break;

+			case 182: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 38ec17fc..6cf71fa1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1190,6 +1190,24 @@ namespace Microsoft.Dafny {
         }

         if (parensNeeded) { wr.Write(")"); }

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write("map ");

+        string sep = "";

+        foreach (BoundVar bv in e.BoundVars) {

+          wr.Write("{0}{1}", sep, bv.Name);

+          sep = ", ";

+          PrintType(": ", bv.Type);

+        }

+        PrintAttributes(e.Attributes);

+        wr.Write(" | ");

+        PrintExpression(e.Range);

+        wr.Write(" :: ");

+        PrintExpression(e.Term);

+        if (parensNeeded) { wr.Write(")"); }

+

       } else if (expr is WildcardExpr) {

         wr.Write("*");

 

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 29a4943a..d966a76f 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -353,6 +353,8 @@ namespace Microsoft.Dafny {
           return new ForallExpr(tk, bvs, range, term, null);

         } else if (e is ExistsExpr) {

           return new ExistsExpr(tk, bvs, range, term, null);

+        } else if (e is MapComprehension) {

+          return new MapComprehension(tk, bvs, range, term);

         } else {

           Contract.Assert(e is SetComprehension);

           return new SetComprehension(tk, bvs, range, term);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 4402e5b1..7be3fca2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3067,6 +3067,42 @@ namespace Microsoft.Dafny {
           }

         }

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        int prevErrorCount = ErrorCount;

+        scope.PushMarker();

+        if (e.BoundVars.Count != 1) {

+          Error(e.tok, "a map comprehension must have exactly one bound variable.");

+        }

+        foreach (BoundVar v in e.BoundVars) {

+          if (!scope.Push(v.Name, v)) {

+            Error(v, "Duplicate bound-variable name: {0}", v.Name);

+          }

+          ResolveType(v.tok, v.Type, null, true);

+        }

+        ResolveExpression(e.Range, twoState);

+        Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.Range.Type, Type.Bool)) {

+          Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);

+        }

+        ResolveExpression(e.Term, twoState);

+        Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

+

+        ResolveAttributes(e.Attributes, twoState);

+        scope.PopMarker();

+        expr.Type = new MapType(e.BoundVars[0].Type,e.Term.Type);

+

+        if (prevErrorCount == ErrorCount) {

+          var missingBounds = new List<BoundVar>();

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          if (missingBounds.Count != 0) {

+            e.MissingBounds = missingBounds;

+            foreach (var bv in e.MissingBounds) {

+              Error(expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+            }

+          }

+        }

+

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

 

@@ -4251,6 +4287,9 @@ namespace Microsoft.Dafny {
       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));

       } else if (expr is WildcardExpr) {

         return false;

       } else if (expr is PredicateExpr) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3f3d89f1..0189c11b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1730,19 +1730,29 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         bool isSequence = e.Seq.Type is SeqType;

-        Bpl.Expr total = IsTotal(e.Seq, etran);

-        Bpl.Expr seq = etran.TrExpr(e.Seq);

-        Bpl.Expr e0 = null;

-        if (e.E0 != null) {

-          e0 = etran.TrExpr(e.E0);

-          total = BplAnd(total, IsTotal(e.E0, etran));

-          total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));

-        }

-        if (e.E1 != null) {

-          total = BplAnd(total, IsTotal(e.E1, etran));

-          total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));

+        if (e.Seq.Type is MapType) {

+          Bpl.Expr total = IsTotal(e.Seq, etran);

+          Bpl.Expr map = etran.TrExpr(e.Seq);

+          var e0 = etran.TrExpr(e.E0);

+          Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), map);

+          inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type));

+          total = BplAnd(total, inDomain);

+          return total;

+        } else {

+          Bpl.Expr total = IsTotal(e.Seq, etran);

+          Bpl.Expr seq = etran.TrExpr(e.Seq);

+          Bpl.Expr e0 = null;

+          if (e.E0 != null) {

+            e0 = etran.TrExpr(e.E0);

+            total = BplAnd(total, IsTotal(e.E0, etran));

+            total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));

+          }

+          if (e.E1 != null) {

+            total = BplAnd(total, IsTotal(e.E1, etran));

+            total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));

+          }

+          return total;

         }

-        return total;

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

         Bpl.Expr total = IsTotal(e.Array, etran);

@@ -5475,7 +5485,7 @@ namespace Microsoft.Dafny {
               x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);

             } else if (e.Seq.Type is MapType) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq);

-              x = Bpl.Expr.Select(x, translator.FunctionCall(e.tok, BuiltinFunction.Box, null, e0));

+              x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));

             } else { Contract.Assert(false); x = null; }

             if (!ModeledAsBoxType(elmtType)) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);

@@ -5839,6 +5849,36 @@ namespace Microsoft.Dafny {
 

           return new Bpl.LambdaExpr(expr.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, exst);

 

+        } else if (expr is MapComprehension) {

+          var e = (MapComprehension)expr;

+          // Translate "map x | R :: T" into

+          // Map#Glue(lambda y: BoxType :: [unbox(y)/x]R,

+          //          lambda y: BoxType :: [unbox(y)/x]T)".

+          Bpl.VariableSeq bvars = new Bpl.VariableSeq();

+          var bv = e.BoundVars[0];

+          TrBoundVariables(e.BoundVars, bvars);

+          

+          Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

+

+          var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));

+          translator.otherTmpVarCount++;

+

+          Bpl.Expr typeAntecedent = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, this);

+          Bpl.Expr unboxy = !ModeledAsBoxType(bv.Type) ? translator.FunctionCall(e.tok, BuiltinFunction.Unbox, translator.TrType(bv.Type), new Bpl.IdentifierExpr(expr.tok, yVar))

+            : (Bpl.Expr)(new Bpl.IdentifierExpr(expr.tok, yVar));

+

+

+          Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();

+          subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));

+

+          var ebody = translator.BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(Substitute(e.Range, null, subst)));

+          Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, ebody);

+          ebody = TrExpr(Substitute(e.Term, null, subst));

+          Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new Bpl.TypeVariableSeq(), new VariableSeq(yVar), kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type));

+

+          

+          return translator.FunctionCall(e.tok, BuiltinFunction.MapGlue, null, l1, l2);

+

         } else if (expr is PredicateExpr) {

           var e = (PredicateExpr)expr;

           return TrExpr(e.Body);

@@ -6301,6 +6341,7 @@ namespace Microsoft.Dafny {
       MapBuild,

       MapDisjoint,

       MapUnion,

+      MapGlue,

 

       IndexField,

       MultiIndexField,

@@ -6485,6 +6526,9 @@ namespace Microsoft.Dafny {
         case BuiltinFunction.MapElements:

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

           return FunctionCall(tok, "Map#Elements", typeInstantiation, args);

+        case BuiltinFunction.MapGlue:

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

+          return FunctionCall(tok, "Map#Glue", predef.MapType(tok, predef.BoxType, predef.BoxType), args);

         case BuiltinFunction.MapEqual:

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

           Contract.Assert(typeInstantiation == null);

@@ -7427,6 +7471,10 @@ namespace Microsoft.Dafny {
           if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

             newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

           }

+        } else if (e is MapComprehension) {

+          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

+            newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+          }

         } else if (e is QuantifierExpr) {

           var q = (QuantifierExpr)e;

           if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

@@ -7437,7 +7485,7 @@ namespace Microsoft.Dafny {
             }

           }

         } else {

-          Contract.Assume(false);  // unexpected ComprehensionExpr

+          Contract.Assert(false);  // unexpected ComprehensionExpr

         }

 

       } else if (expr is PredicateExpr) {

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
index 80d97ebc..6521960c 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -195,11 +195,13 @@ class BlockPredicator {
     foreach (var decl in p.TopLevelDeclarations) {
       if (decl is DeclWithFormals && !(decl is Function)) {
         var dwf = (DeclWithFormals)decl;
-        var fpVar = new LocalVariable(Token.NoToken,
-                                    new TypedIdent(Token.NoToken, "fp",
-                                                   Microsoft.Boogie.Type.Bool));
-        dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar))
-                       .Cast<Variable>().ToArray());
+        var fpVar = new Formal(Token.NoToken,
+                               new TypedIdent(Token.NoToken, "fp",
+                                              Microsoft.Boogie.Type.Bool),
+                               /*incoming=*/true);
+        dwf.InParams = new VariableSeq(
+          (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
+            .ToArray());
       }
       var impl = decl as Implementation;
       if (impl != null)
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 27ec052e..4e30951e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -1403,6 +1403,9 @@ namespace GPUVerify
             StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);

             Implementation BarrierImplementation = new Implementation(BarrierProcedure.tok, BarrierProcedure.Name, new TypeVariableSeq(), BarrierProcedure.InParams, BarrierProcedure.OutParams, new VariableSeq(), statements);

 

+            if (CommandLineOptions.Unstructured)

+                BarrierImplementation.Resolve(ResContext);

+

             BarrierImplementation.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });

             BarrierProcedure.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });

 

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index d753762f..19ec088d 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -245,6 +245,11 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+  public class Macro : Function {

+    public Macro(IToken tok, string name, VariableSeq args, Variable result)

+      : base(tok, name, args, result) { }

+  }

+

   public class InlineRequiresVisitor : StandardVisitor {

     public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

       Contract.Requires(cmdSeq != null);

@@ -279,11 +284,6 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

-  public class Macro : Function {

-    public Macro(IToken tok, string name, VariableSeq args, Variable result)

-      : base(tok, name, args, result) { }

-  }

-

   public class FreeRequiresVisitor : StandardVisitor {

     public override Requires VisitRequires(Requires requires) {

       if (requires.Free)

@@ -301,6 +301,13 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

+  public class InlineEnsuresVisitor : StandardVisitor {

+    public override Ensures VisitEnsures(Ensures ensures) {

+      ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);

+      return base.VisitEnsures(ensures);

+    }

+  }

+

   public class Houdini : ObservableHoudini {

     private Program program;

     private HashSet<Variable> houdiniConstants;

@@ -367,6 +374,11 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       foreach (Implementation impl in callGraph.Nodes) {

+        InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();

+        inlineEnsuresVisitor.Visit(impl);

+      }

+

+      foreach (Implementation impl in callGraph.Nodes) {

         impl.OriginalBlocks = impl.Blocks;

         impl.OriginalLocVars = impl.LocVars;

       }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 35a5017b..c451cc62 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1565,7 +1565,7 @@ Maps.dfy(126,13): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 22 verified, 2 errors

+Dafny program verifier finished with 30 verified, 2 errors

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy
index eb543283..a49ac3c1 100644
--- a/Test/dafny0/Maps.dfy
+++ b/Test/dafny0/Maps.dfy
@@ -2,7 +2,7 @@
 // This method can be used to test compilation.

 method Main()

 {

-   var m:= map{2:=3};

+   var m := map[2:=3];

    // test "in"

    if(2 in m)

    {

@@ -25,28 +25,28 @@ method Main()
    else

    { assert false; }

    // test disjoint operator

-   if(m !! map{3 := 3})

+   if(m !! map[3 := 3])

    {

       print "m3\n";

    }

    else

    { assert false; }

    // updates should replace values that already exist

-   if(m[2 := 4] == map{2 := 4})

+   if(m[2 := 4] == map[2 := 4])

    {

       print "m4\n";

    }

    else

    { assert false; }

    // add something to the map

-   if(m[7 := 1] == map{2 := 3,7 := 1})

+   if(m[7 := 1] == map[2 := 3,7 := 1])

    {

       print "m5\n";

    }

    else

    { assert false; }

    // test applicative nature of Map<U, V> in C#

-   if(m == map{2 := 3})

+   if(m == map[2 := 3])

    {

       print "m6\n";

    }

@@ -57,7 +57,7 @@ method Main()
 

 method m()

 {

-   var a := map{2:=3}; var b := map{3:=2};

+   var a := map[2:=3]; var b := map[3:=2];

    assert a[b[3]] == 3;

 }

 method m2(a: map<int, bool>, b: map<int, bool>)

@@ -72,7 +72,7 @@ method m3(a: map<int, int>)
 }

 method m4()

 {

-   var a := map{3 := 9};

+   var a := map[3 := 9];

    if(a[4] == 4) // UNSAFE, 4 not in the domain

    {

       m();

@@ -86,14 +86,14 @@ method m5(a: map<int, int>)
 }

 method m6()

 {

-   var a := map{3 := 9};

-   assert a[3:=5] == map{3:=5};

-   assert a[2:=5] == map{2:=5, 3:=9};

-   assert a[2:=5] == map{2:=6, 3:=9, 2:=5}; // test the ordering of assignments in the map literal

+   var a := map[3 := 9];

+   assert a[3:=5] == map[3:=5];

+   assert a[2:=5] == map[2:=5, 3:=9];

+   assert a[2:=5] == map[2:=6, 3:=9, 2:=5]; // test the ordering of assignments in the map literal

 }

 method m7()

 {

-   var a := map{1:=1, 2:=4, 3:=9};

+   var a := map[1:=1, 2:=4, 3:=9];

    assert forall i | i in a :: a[i] == i * i;

    assert 0 !in a;

    assert 1 in a;

@@ -103,7 +103,7 @@ method m7()
 }

 method m8()

 {

-   var a := map{};

+   var a := map[];

    assert forall i :: i !in a; // check emptiness

    var i,n := 0, 100;

    while(i < n)

@@ -114,24 +114,24 @@ method m8()
       a := a[i := i * i];

       i := i + 1;

    }

-   assert a !! map{-1:=2};

+   assert a !! map[-1:=2];

    m3(a);

 }

 method m9()

 {

-   var a, b := map{}, map{};

+   var a, b := map[], map[];

    assert a !! b;

-   b := map{2:=3,4:=2,5:=-6,6:=7};

+   b := map[2:=3,4:=2,5:=-6,6:=7];

    assert a !! b;

-   assert b !! map{6:=3}; // ERROR, both share 6 in the domain.

+   assert b !! map[6:=3]; // ERROR, both share 6 in the domain.

 }

 method m10()

 {

-   var a, b := map{}, map{};

+   var a, b := map[], map[];

    assert a !! b;

-   b := map{2:=3,4:=2,5:=-6,6:=7};

+   b := map[2:=3,4:=2,5:=-6,6:=7];

    assert a !! b;

-   a := map{3:=3,1:=2,9:=-6,8:=7};

+   a := map[3:=3,1:=2,9:=-6,8:=7];

    assert a !! b;

 }

 method m11<U, V>(a: map<U, V>, b: map<U, V>)

@@ -139,3 +139,44 @@ method m11<U, V>(a: map<U, V>, b: map<U, V>)
 {

    assert a !! b;

 }

+

+method m12()

+{

+   var x := map i | 0 <= i < 10 :: i * 2;

+   assert 0 in x;

+   assert 1 in x;

+   assert 10 !in x;

+   assert x[0] == 0 && x[2] == 4;

+}

+

+function domain<U, V>(m: map<U,V>): set<U>

+   ensures forall i :: i in domain(m) <==> i in m;

+{

+   set s | s in m

+}

+

+method m13()

+{

+   var s := {0, 1, 3, 4};

+   var x := map i | i in s :: i;

+   assert forall i | i in x :: x[i] == i;

+   assert domain(x) == s;

+}

+

+function union<U, V>(m: map<U,V>, m': map<U,V>): map<U,V>

+   requires m !! m';

+   ensures forall i :: i in union(m, m') <==> i in m || i in m';

+   ensures forall i :: i in m ==> union(m, m')[i] == m[i];

+   ensures forall i :: i in m' ==> union(m, m')[i] == m'[i];

+{

+   map i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i]

+}

+

+method m14()

+{

+   var s, t := {0, 1}, {3, 4};

+   var x,y := map i | i in s :: i, map i | i in t :: 1+i;

+   ghost var u := union(x,y);

+   assert u[1] == 1 && u[3] == 4;

+   assert domain(u) == {0, 1, 3, 4};

+}

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index b9083fae..48ca65e9 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4
 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

+Stratified Inlining: Reached recursion bound of 4

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl
new file mode 100644
index 00000000..8388cd57
--- /dev/null
+++ b/Test/extractloops/detLoopExtract1.bpl
@@ -0,0 +1,30 @@
+var g:int;
+
+procedure {:entrypoint} Foo(a:int)
+requires a >= 0;
+modifies g;
+{
+   var b: int;
+   b := 0;
+   g := a;
+  
+LH:
+   goto L_true, L_false;
+
+L_true:
+   assume (b < a); 
+   goto L6;
+
+L6: 
+  b := b + 1;
+  g := 5;
+  goto LH;
+
+L_false:
+   assume (b >= a);	      
+   goto L_end;
+
+L_end:
+   assume (b != a); //modeling assert for stratified inlining
+   return;
+}
diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index 05bfae55..6bd151cb 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -19,4 +19,7 @@ echo -----
 echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops

 %BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl

 echo -----

+echo ----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

+%BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract1.bpl

+echo -----

 

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 81442950..92432858 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,20 +1,20 @@
-# Aste started: 2012-05-30 07:00:05

+# Aste started: 2012-06-02 07:00:02

 # Host id: Boogiebox

 # Configuration: boogie.cfg

 # Task: aste.tasks.boogie.FullBuild

-# [2012-05-30 07:01:49] SpecSharp revision: f992747219c4

-# [2012-05-30 07:01:49] SscBoogie revision: f992747219c4

-# [2012-05-30 07:02:37] Boogie revision: c78721acaf27

-[2012-05-30 07:04:36] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

+# [2012-06-02 07:01:16] SpecSharp revision: 219e6b40fa91

+# [2012-06-02 07:01:16] SscBoogie revision: 219e6b40fa91

+# [2012-06-02 07:02:04] Boogie revision: ee3b87304b4b

+[2012-06-02 07:03:58] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build

 

     1>corflags : warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


     warning CF011: The specified file is strong name signed.  Using /Force will invalidate the signature of this image and will require the assembly to be resigned.


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

+[2012-06-02 07:05:24] 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\Absy.cs(748,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\Absy.cs(751,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)'.


     EXEC : warning CC1079: Type Microsoft.Boogie.Variable implements Microsoft.AbstractInterpretationFramework.IVariable.get_Name by inheriting Microsoft.Boogie.NamedDeclaration.get_Name causing the interface contract to not be checked at runtime. Consider adding a wrapper method.


     D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,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(121,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.


@@ -41,5 +41,5 @@
     warning CS0162: Unreachable code detected


     warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.


     warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.


-[2012-05-30 08:07:19] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2012-05-30 08:08:25] Released nightly of Boogie

+[2012-06-02 08:02:40] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2012-06-02 08:03:32] Released nightly of Boogie