diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
| commit | 7b8adafdc184fd812fbb26d4d4ca4aaf5f0d134a (patch) | |
| tree | 727566ae9586fa19d32c71b3872a57392ce9cd0f /Dafny/Compiler.cs | |
| parent | 7cf0e87a3c9cbc769a9248604e8943a7faddd914 (diff) | |
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 72 |
1 files changed, 37 insertions, 35 deletions
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;
|