Merge

10 files changed, 125 insertions, 49 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 0e599ad2..8552e480 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -363,7 +363,7 @@ namespace Microsoft.Dafny
 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

-        return new LetExpr(Tok(e.tok), e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact);

+        return new LetExpr(Tok(e.tok), e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact, e.Attributes);

 

       } else if (expr is NamedExpr) {

         var e = (NamedExpr)expr;

@@ -385,13 +385,13 @@ namespace Microsoft.Dafny
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected quantifier expression

           }

         } else if (e is MapComprehension) {

-          return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term);

+          return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term, CloneAttributes(e.Attributes));

         } else if (e is LambdaExpr) {

           var l = (LambdaExpr)e;

           return new LambdaExpr(tk, l.OneShot, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term);

         } else {

           Contract.Assert(e is SetComprehension);

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

+          return new SetComprehension(tk, bvs, range, term, CloneAttributes(e.Attributes));

         }

 

       } else if (expr is WildcardExpr) {

@@ -540,7 +540,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

-        r = new AssignSuchThatStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));

+        r = new AssignSuchThatStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken), null);

 

       } else if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index dc26392b..a9653439 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1484,7 +1484,7 @@ UpdateStmt<out Statement/*!*/ s>
   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

   )

   (. if (suchThat != null) {

-       s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);

+       s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume, null);

      } else {

        if (lhss.Count == 0 && rhss.Count == 0) {

          s = new BlockStmt(x, endTok, new List<Statement>()); // error, give empty statement

@@ -1552,7 +1552,8 @@ VarDeclStatement<.out Statement/*!*/ s.>
     Rhs<out r>                     (. rhss.Add(r); .)

     { "," Rhs<out r>               (. rhss.Add(r); .)

     }

-  | ":|"                           (. assignTok = t; .)

+  | { Attribute<ref attrs> }

+    ":|"                           (. assignTok = t; .)

     [ IF(la.kind == _assume)       /* an Expression can also begin with an "assume", so this says to resolve it to pick up any "assume" here */

       "assume"                     (. suchThatAssume = t; .)

     ]

@@ -1565,7 +1566,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
        foreach (var lhs in lhss) {

          ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));

        }

-       update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume);

+       update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs);

      } else if (rhss.Count == 0) {

        update = null;

      } else {

@@ -2429,12 +2430,14 @@ MapComprehensionExpr<IToken mapToken, bool finite, out Expression e, bool allowS
      List<BoundVar> bvars = new List<BoundVar>();

      Expression range = null;

      Expression body;

+     Attributes attrs = null;

   .)

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

+  { Attribute<ref attrs> }

   [ "|" Expression<out range, true, true> ]

   QSep

   Expression<out body, allowSemi, allowLambda>

-  (. e = new MapComprehension(mapToken, finite, bvars, range ?? new LiteralExpr(mapToken, true), body);

+  (. e = new MapComprehension(mapToken, finite, bvars, range ?? new LiteralExpr(mapToken, true), body, attrs);

   .)

   .

 EndlessExpression<out Expression e, bool allowSemi, bool allowLambda>

@@ -2476,6 +2479,7 @@ LetExpr<out Expression e, bool allowSemi, bool allowLambda>
      var letRHSs = new List<Expression>();

      CasePattern pat;

      bool exact = true;

+     Attributes attrs = null;

      e = dummyExpr;

   .)

     [ "ghost"                       (. isGhost = true;  x = t; .)

@@ -2489,7 +2493,8 @@ LetExpr<out Expression e, bool allowSemi, bool allowLambda>
                                     .)

     }

     ( ":="

-    | ":|"                          (. exact = false;

+    | { Attribute<ref attrs> }

+      ":|"                          (. exact = false;

                                        foreach (var lhs in letLHSs) {

                                          if (lhs.Arguments != null) {

                                            SemErr(lhs.tok, "LHS of let-such-that expression must be variables, not general patterns");

@@ -2501,7 +2506,7 @@ LetExpr<out Expression e, bool allowSemi, bool allowLambda>
     { "," Expression<out e, false, true>  (. letRHSs.Add(e); .)

     }

     ";"

-    Expression<out e, allowSemi, allowLambda>    (. e = new LetExpr(x, letLHSs, letRHSs, e, exact); .)

+    Expression<out e, allowSemi, allowLambda>    (. e = new LetExpr(x, letLHSs, letRHSs, e, exact, attrs); .)

   .

 

 NamedExpr<out Expression e, bool allowSemi, bool allowLambda>

@@ -2775,19 +2780,21 @@ SetComprehensionExpr<out Expression q, bool allowSemi, bool allowLambda>
      List<BoundVar/*!*/> bvars = new List<BoundVar>();

      Expression range;

      Expression body = null;

+     Attributes attrs = null;

   .)

   "set"                                        (. x = t; .)

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

   { ","

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

   }

+  { Attribute<ref attrs> }

   "|" Expression<out range, allowSemi, allowLambda>

   [ IF(IsQSep())  /* let any given body bind to the closest enclosing set comprehension */

     QSep

     Expression<out body, allowSemi, allowLambda>

   ]

   (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

-     q = new SetComprehension(x, bvars, range, body);

+     q = new SetComprehension(x, bvars, range, body, attrs);

   .)

   .

 Expressions<.List<Expression> args.>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 8893f189..14c1b35e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3709,8 +3709,8 @@ namespace Microsoft.Dafny {
   public abstract class ConcreteUpdateStatement : Statement

   {

     public readonly List<Expression> Lhss;

-    public ConcreteUpdateStatement(IToken tok, IToken endTok, List<Expression> lhss)

-      : base(tok, endTok) {

+    public ConcreteUpdateStatement(IToken tok, IToken endTok, List<Expression> lhss, Attributes attrs = null)

+      : base(tok, endTok, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

       Contract.Requires(cce.NonNullElements(lhss));

@@ -3738,8 +3738,8 @@ namespace Microsoft.Dafny {
     /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.

     /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement.

     /// </summary>

-    public AssignSuchThatStmt(IToken tok, IToken endTok, List<Expression> lhss, Expression expr, IToken assumeToken)

-      : base(tok, endTok, lhss) {

+    public AssignSuchThatStmt(IToken tok, IToken endTok, List<Expression> lhss, Expression expr, IToken assumeToken, Attributes attrs)

+      : base(tok, endTok, lhss, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(endTok != null);

       Contract.Requires(cce.NonNullElements(lhss));

@@ -6282,20 +6282,25 @@ namespace Microsoft.Dafny {
     public readonly List<Expression> RHSs;

     public readonly Expression Body;

     public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression

+    public readonly Attributes Attributes;

     public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for a ghost statement

     // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;

     public List<IVariable> Constraint_MissingBounds;  // filled in during resolution; remains "null" if Exact==true or if bounds can be found

     // invariant Constraint_Bounds == null || Constraint_MissingBounds == null;

     public Expression translationDesugaring;  // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true

-    public LetExpr(IToken tok, List<CasePattern> lhss, List<Expression> rhss, Expression body, bool exact)

+    public LetExpr(IToken tok, List<CasePattern> lhss, List<Expression> rhss, Expression body, bool exact, Attributes attrs = null)

       : base(tok) {

       LHSs = lhss;

       RHSs = rhss;

       Body = body;

       Exact = exact;

+      Attributes = attrs;

     }

     public override IEnumerable<Expression> SubExpressions {

       get {

+        foreach (var e in Attributes.SubExpressions(Attributes)) {

+          yield return e;

+        }

         foreach (var rhs in RHSs) {

           yield return rhs;

         }

@@ -6537,8 +6542,8 @@ namespace Microsoft.Dafny {
   {

     public readonly bool TermIsImplicit;

 

-    public SetComprehension(IToken tok, List<BoundVar> bvars, Expression range, Expression term)

-      : base(tok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), null) {

+    public SetComprehension(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

+      : base(tok, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) {

       Contract.Requires(tok != null);

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

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

@@ -6551,8 +6556,8 @@ namespace Microsoft.Dafny {
   {

     public readonly bool Finite;

 

-    public MapComprehension(IToken tok, bool finite, List<BoundVar> bvars, Expression range, Expression term)

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

+    public MapComprehension(IToken tok, bool finite, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)

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

       Contract.Requires(tok != null);

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

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

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 3426da4c..6342e9c7 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2194,7 +2194,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

 		} else SynErr(179);

 		if (suchThat != null) {

-		 s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);

+		 s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume, null);

 		} else {

 		 if (lhss.Count == 0 && rhss.Count == 0) {

 		   s = new BlockStmt(x, endTok, new List<Statement>()); // error, give empty statement

@@ -2235,7 +2235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); d.Attributes = attrs; attrs = null; 

 		}

-		if (la.kind == 91 || la.kind == 93) {

+		if (la.kind == 39 || la.kind == 91 || la.kind == 93) {

 			if (la.kind == 91) {

 				Get();

 				assignTok = t; 

@@ -2247,7 +2247,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					rhss.Add(r); 

 				}

 			} else {

-				Get();

+				while (la.kind == 39) {

+					Attribute(ref attrs);

+				}

+				Expect(93);

 				assignTok = t; 

 				if (la.kind == _assume) {

 					Expect(29);

@@ -2265,7 +2268,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 foreach (var lhs in lhss) {

 		   ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));

 		 }

-		 update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume);

+		 update = new AssignSuchThatStmt(assignTok, endTok, ies, suchThat, suchThatAssume, attrs);

 		} else if (rhss.Count == 0) {

 		 update = null;

 		} else {

@@ -3896,16 +3899,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> bvars = new List<BoundVar>();

 		Expression range = null;

 		Expression body;

+		Attributes attrs = null;

 		

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

+		while (la.kind == 39) {

+			Attribute(ref attrs);

+		}

 		if (la.kind == 22) {

 			Get();

 			Expression(out range, true, true);

 		}

 		QSep();

 		Expression(out body, allowSemi, allowLambda);

-		e = new MapComprehension(mapToken, finite, bvars, range ?? new LiteralExpr(mapToken, true), body);

+		e = new MapComprehension(mapToken, finite, bvars, range ?? new LiteralExpr(mapToken, true), body, attrs);

 		

 	}

 

@@ -3967,6 +3974,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar/*!*/> bvars = new List<BoundVar>();

 		Expression range;

 		Expression body = null;

+		Attributes attrs = null;

 		

 		Expect(13);

 		x = t; 

@@ -3977,6 +3985,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out bv);

 			bvars.Add(bv); 

 		}

+		while (la.kind == 39) {

+			Attribute(ref attrs);

+		}

 		Expect(22);

 		Expression(out range, allowSemi, allowLambda);

 		if (IsQSep()) {

@@ -3984,7 +3995,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out body, allowSemi, allowLambda);

 		}

 		if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

-		q = new SetComprehension(x, bvars, range, body);

+		q = new SetComprehension(x, bvars, range, body, attrs);

 		

 	}

 

@@ -4006,6 +4017,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		var letRHSs = new List<Expression>();

 		CasePattern pat;

 		bool exact = true;

+		Attributes attrs = null;

 		e = dummyExpr;

 		

 		if (la.kind == 65) {

@@ -4027,8 +4039,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		if (la.kind == 91) {

 			Get();

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

-			Get();

+		} else if (la.kind == 39 || la.kind == 93) {

+			while (la.kind == 39) {

+				Attribute(ref attrs);

+			}

+			Expect(93);

 			exact = false;

 			foreach (var lhs in letLHSs) {

 			 if (lhs.Arguments != null) {

@@ -4046,7 +4061,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(26);

 		Expression(out e, allowSemi, allowLambda);

-		e = new LetExpr(x, letLHSs, letRHSs, e, exact); 

+		e = new LetExpr(x, letLHSs, letRHSs, e, exact, attrs); 

 	}

 

 	void NamedExpr(out Expression e, bool allowSemi, bool allowLambda) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index eaa4197e..2af9729b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -570,7 +570,7 @@ namespace Microsoft.Dafny
             {

               ResolvedOp = BinaryExpr.ResolvedOpcode.InSet,

               Type = Type.Bool

-            }, obj)

+            }, obj, null)

           {

             Type = new SetType(new ObjectType())

           };

@@ -610,7 +610,7 @@ namespace Microsoft.Dafny
             var sInE = new BinaryExpr(e.tok, BinaryExpr.Opcode.In, bvIE, e);

             sInE.ResolvedOp = BinaryExpr.ResolvedOpcode.InSeq;  // resolve here

             sInE.Type = Type.Bool;  // resolve here

-            var s = new SetComprehension(e.tok, new List<BoundVar>() { bv }, sInE, bvIE);

+            var s = new SetComprehension(e.tok, new List<BoundVar>() { bv }, sInE, bvIE, null);

             s.Type = new SetType(new ObjectType());  // resolve here

             sets.Add(s);

           } else {

@@ -5369,6 +5369,7 @@ namespace Microsoft.Dafny
       } else {

         ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs);

       }

+      ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));

     }

     /// <summary>

     /// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller).

@@ -7065,6 +7066,7 @@ namespace Microsoft.Dafny
           }

         }

         ResolveExpression(e.Body, opts);

+        ResolveAttributes(e.Attributes, opts);

         scope.PopMarker();

         expr.Type = e.Body.Type;

 

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index d981a7a1..cbe8e6e5 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -217,7 +217,7 @@ public class Scanner {
 

 	[ContractInvariantMethod]

 	void objectInvariant(){

-		Contract.Invariant(buffer!=null);

+		Contract.Invariant(this._buffer != null);

 		Contract.Invariant(t != null);

 		Contract.Invariant(start != null);

 		Contract.Invariant(tokens != null);

@@ -227,7 +227,18 @@ public class Scanner {
 		Contract.Invariant(errorHandler != null);

 	}

 

-	public Buffer/*!*/ buffer; // scanner buffer

+	private Buffer/*!*/ _buffer; // scanner buffer

+

+	public Buffer/*!*/ buffer {

+		get {

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

+			return this._buffer;

+		}

+		set {

+			Contract.Requires(value != null);

+			this._buffer = value;

+		}

+	}

 

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

@@ -307,7 +318,7 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

-			buffer = new Buffer(stream, false);

+			this._buffer = new Buffer(stream, false);

 			Filename = useBaseName? GetBaseName(fileName): fileName;

 			Init();

 		} catch (IOException) {

@@ -322,7 +333,7 @@ public class Scanner {
 	  Contract.Requires(fileName != null);

 		pt = tokens = new Token();  // first token is a dummy

 		t = new Token(); // dummy because t is a non-null field

-		buffer = new Buffer(s, true);

+		this._buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

 		Init();

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f0baeef3..a150eecd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4453,7 +4453,12 @@ namespace Microsoft.Dafny {
         if (canCall != Bpl.Expr.True) {

           List<Variable> bvars = new List<Variable>();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

-          canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), Bpl.Expr.Imp(typeAntecedent, canCall));

+          if (Attributes.Contains(e.Attributes, "trigger")) {

+            Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok);

+            canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), tr, Bpl.Expr.Imp(typeAntecedent, canCall));

+          } else {

+            canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), Bpl.Expr.Imp(typeAntecedent, canCall));

+          }

         }

         return canCall;

       } else if (expr is StmtExpr) {

@@ -4863,7 +4868,8 @@ namespace Microsoft.Dafny {
           Formal p = e.Function.Formals[i];

           // Note, in the following, the "##" makes the variable invisible in BVD.  An alternative would be to communicate

           // to BVD what this variable stands for and display it as such to the user.

-          LocalVariable local = new LocalVariable(p.tok, p.tok, "##" + p.Name, p.Type, p.IsGhost);

+          Type et = Resolver.SubstType(p.Type, e.TypeArgumentSubstitutions);

+          LocalVariable local = new LocalVariable(p.tok, p.tok, "##" + p.Name, et, p.IsGhost);

           local.type = local.OptionalType;  // resolve local here

           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator));

           ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -4871,9 +4877,8 @@ namespace Microsoft.Dafny {
           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))));

           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

           Expression ee = e.Args[i];

-          Type et = Resolver.SubstType(p.Type, e.TypeArgumentSubstitutions);

           CheckSubrange(ee.tok, etran.TrExpr(ee), et, builder);

-          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type));

+          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), et));

           builder.Add(cmd);

           builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));

           builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

@@ -5096,7 +5101,8 @@ namespace Microsoft.Dafny {
             if (tup.Item1.Count != 0) {

               var bvs = new List<Variable>();

               var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

-              body = new Bpl.ExistsExpr(e.tok, bvs, BplAnd(typeAntecedent, body));

+              var triggers = TrTrigger(etran, e.Attributes, e.tok);

+              body = new Bpl.ExistsExpr(e.tok, bvs, triggers, BplAnd(typeAntecedent, body));

             }

             w = BplOr(body, w);

           }

@@ -7050,7 +7056,8 @@ namespace Microsoft.Dafny {
             if (tup.Item1.Count != 0) {

               var bvs = new List<Variable>();

               var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

-              body = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, body));

+              var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap);

+              body = new Bpl.ExistsExpr(s.Tok, bvs, triggers, BplAnd(typeAntecedent, body));

             }

             w = BplOr(body, w);

           }

@@ -8241,7 +8248,8 @@ namespace Microsoft.Dafny {
 

       Bpl.Expr qq = Bpl.Expr.Imp(ante, post);

       if (bvars.Count != 0) {

-        qq = new Bpl.ForallExpr(s.Tok, bvars, qq);

+        var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap);

+        qq = new Bpl.ForallExpr(s.Tok, bvars, triggers, qq);

       }

       exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));

     }

@@ -11187,14 +11195,15 @@ namespace Microsoft.Dafny {
           // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".

           List<Variable> bvars = new List<Variable>();

           Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);

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

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

 

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

           Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);

 

           var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));

           var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range)), eq);

-          var exst = new Bpl.ExistsExpr(expr.tok, bvars, ebody);

+          var triggers = translator.TrTrigger(this, e.Attributes, e.tok);

+          var exst = new Bpl.ExistsExpr(expr.tok, bvars, triggers, ebody);

 

           return new Bpl.LambdaExpr(expr.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, exst);

 

@@ -11208,7 +11217,7 @@ namespace Microsoft.Dafny {
           var bv = e.BoundVars[0];

           TrBoundVariables(e.BoundVars, bvars);

 

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

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

 

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

 

@@ -13417,9 +13426,9 @@ namespace Microsoft.Dafny {
           Attributes newAttrs = SubstAttributes(e.Attributes);

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

             if (e is SetComprehension) {

-              newExpr = new SetComprehension(expr.tok, newBoundVars, newRange, newTerm);

+              newExpr = new SetComprehension(expr.tok, newBoundVars, newRange, newTerm, newAttrs);

             } else if (e is MapComprehension) {

-              newExpr = new MapComprehension(expr.tok, ((MapComprehension)e).Finite, newBoundVars, newRange, newTerm);

+              newExpr = new MapComprehension(expr.tok, ((MapComprehension)e).Finite, newBoundVars, newRange, newTerm, newAttrs);

             } else if (expr is ForallExpr) {

               newExpr = new ForallExpr(expr.tok, ((QuantifierExpr)expr).TypeArgs, newBoundVars, newRange, newTerm, newAttrs);

             } else if (expr is ExistsExpr) {

@@ -13697,7 +13706,7 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is AssignSuchThatStmt) {

           var s = (AssignSuchThatStmt)stmt;

-          r = new AssignSuchThatStmt(s.Tok, s.EndTok, s.Lhss.ConvertAll(Substitute), Substitute(s.Expr), s.AssumeToken == null ? null : s.AssumeToken);

+          r = new AssignSuchThatStmt(s.Tok, s.EndTok, s.Lhss.ConvertAll(Substitute), Substitute(s.Expr), s.AssumeToken == null ? null : s.AssumeToken, null);

         } else if (stmt is UpdateStmt) {

           var s = (UpdateStmt)stmt;

           var resolved = s.ResolvedStatements;

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 5dd6d8ab..5b8cc943 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -41,7 +41,25 @@ namespace DafnyLanguage
         options.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

         options.ModelViewFile = "-";

         Dafny.DafnyOptions.Install(options);

-        options.ApplyDefaultOptions();

+

+        // Read additional options from DafnyOptions.txt

+        string codebase = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

+        string optionsFilePath = Path.Combine(codebase, "DafnyOptions.txt");

+        if (File.Exists(optionsFilePath)) {

+          var optionsReader = new StreamReader(new FileStream(optionsFilePath, FileMode.Open, FileAccess.Read));

+          List<string> args = new List<string>();

+          while (true) {

+            string line = optionsReader.ReadLine();

+            if (line == null) break;

+            line = line.Trim();

+            if (line.Length == 0 || line.StartsWith("//")) continue;

+            args.Add(line);

+          }

+          optionsReader.Close();

+          CommandLineOptions.Clo.Parse(args.ToArray());

+        } else {

+          options.ApplyDefaultOptions();

+        }

 

         ExecutionEngine.printer = new DummyPrinter();

         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 05bcc503..7b4ec261 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -183,6 +183,9 @@
     <Compile Include="..\version.cs" />

   </ItemGroup>

   <ItemGroup>

+    <Content Include="DafnyOptions.txt">

+      <IncludeInVSIX>true</IncludeInVSIX>

+    </Content>

     <Content Include="DafnyPrelude.bpl">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

@@ -220,6 +223,9 @@
       <Install>false</Install>

     </BootstrapperPackage>

   </ItemGroup>

+  <ItemGroup>

+    <WCFMetadata Include="Service References\" />

+  </ItemGroup>

   <PropertyGroup>

     <UseCodebase>true</UseCodebase>

   </PropertyGroup>

diff --git a/Source/DafnyExtension/DafnyOptions.txt b/Source/DafnyExtension/DafnyOptions.txt
new file mode 100644
index 00000000..e19fe525
--- /dev/null
+++ b/Source/DafnyExtension/DafnyOptions.txt
@@ -0,0 +1,3 @@
+// DafnyLanguageService.vsix copies this file to the Dafny Visual Studio Extension directory

+// Each line contains one command-line argument to the Dafny Visual Studio Extension

+// Blank lines and lines beginning with "//" are ignored