From 7b8adafdc184fd812fbb26d4d4ca4aaf5f0d134a Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 28 May 2011 18:51:27 -0700
Subject: Dafny: changed syntax of havoc statements from "havoc X;" to "X :=
 *;"

---
 Dafny/Compiler.cs | 72 ++++++++++++++++++++++++++++---------------------------
 1 file changed, 37 insertions(+), 35 deletions(-)

(limited to 'Dafny/Compiler.cs')

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 0fbeb9d6..a0629983 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -622,42 +622,44 @@ namespace Microsoft.Dafny {
         AssignStmt s = (AssignStmt)stmt;
         if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
           SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;
-          // Generate the following:
-          //   tmpArr = sel.Seq;
-          //   tmpLow = sel.E0;  // or 0 if sel.E0==null
-          //   tmpHigh = sel.Eq;  // or arr.Length if sel.E1==null
-          //   tmpRhs = s.Rhs;
-          //   for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {
-          //     tmpArr[tmpI] = tmpRhs;
-          //   }
-          string arr = "_arr" + tmpVarCount;
-          string low = "_low" + tmpVarCount;
-          string high = "_high" + tmpVarCount;
-          string rhs = "_rhs" + tmpVarCount;
-          string i = "_i" + tmpVarCount;
-          tmpVarCount++;
-          Indent(indent);  wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Seq.Type)), arr);  TrExpr(sel.Seq);  wr.WriteLine(";");
-          Indent(indent);  wr.Write("int {0} = ", low);
-          if (sel.E0 == null) {
-            wr.Write("0");
-          } else {
-            TrExpr(sel.E0);
-          }
-          wr.WriteLine(";");
-          Indent(indent);  wr.Write("int {0} = ", high);
-          if (sel.E1 == null) {
-            wr.Write("new BigInteger(arr.Length)");
-          } else {
-            TrExpr(sel.E1);
+          if (!(s.Rhs is HavocRhs)) {
+            // Generate the following:
+            //   tmpArr = sel.Seq;
+            //   tmpLow = sel.E0;  // or 0 if sel.E0==null
+            //   tmpHigh = sel.Eq;  // or arr.Length if sel.E1==null
+            //   tmpRhs = s.Rhs;
+            //   for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {
+            //     tmpArr[tmpI] = tmpRhs;
+            //   }
+            string arr = "_arr" + tmpVarCount;
+            string low = "_low" + tmpVarCount;
+            string high = "_high" + tmpVarCount;
+            string rhs = "_rhs" + tmpVarCount;
+            string i = "_i" + tmpVarCount;
+            tmpVarCount++;
+            Indent(indent); wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Seq.Type)), arr); TrExpr(sel.Seq); wr.WriteLine(";");
+            Indent(indent); wr.Write("int {0} = ", low);
+            if (sel.E0 == null) {
+              wr.Write("0");
+            } else {
+              TrExpr(sel.E0);
+            }
+            wr.WriteLine(";");
+            Indent(indent); wr.Write("int {0} = ", high);
+            if (sel.E1 == null) {
+              wr.Write("new BigInteger(arr.Length)");
+            } else {
+              TrExpr(sel.E1);
+            }
+            wr.WriteLine(";");
+            Indent(indent); wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Type)), rhs); TrAssignmentRhs(s.Rhs); wr.WriteLine(";");
+            Indent(indent);
+            wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);
+            Indent(indent + IndentAmount);
+            wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);
+            Indent(indent);
+            wr.WriteLine(";");
           }
-          wr.WriteLine(";");
-          Indent(indent);  wr.Write("{0} {1} = ", TypeName(cce.NonNull(sel.Type)), rhs);  TrAssignmentRhs(s.Rhs);  wr.WriteLine(";");
-          Indent(indent);
-          wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);
-          Indent(indent + IndentAmount);
-          wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);
-          Indent(indent);
-          wr.WriteLine(";");
 
         } else {
           var tRhs = s.Rhs as TypeRhs;
-- 
cgit v1.2.3