From 6027c65707f6098bec2e373b738d80b96cbc0a15 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 29 Oct 2011 16:59:46 -0700
Subject: Dafny induction: * implemented induction tactic for result-less,
 non-mutating ghost methods * refine heuristics for determining if a variables
 is usefully passed to a recursive function * disallow certain "ensures" to
 use two-state features (needed for soundness of the parallel-statement
 translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) *
 added command-line flags /induction and /inductionHeuristic (everything is on
 by default)

---
 Source/Dafny/Dafny.atg | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Source/Dafny/Dafny.atg')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9de1421b..fa857aad 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -922,6 +922,7 @@ ParallelStmt<out Statement/*!*/ s>
   "parallel"                                (. x = t; .)
   "("
   QuantifierDomain<out bvars, out attrs, out range>
+                                            (. if (range == null) { range = new LiteralExpr(x, true); } .)
   ")"
   {                                         (. isFree = false; .)
     [ "free"                                (. isFree = true; .)
-- 
cgit v1.2.3