diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-07-09 12:38:32 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-07-09 12:38:32 -0700 |
| commit | 0251bc077fbfce58f0fa80dc04ba2ee8088f2686 (patch) | |
| tree | be083e7d6b504796f2a3f26add1c63602c52da6f /Source | |
| parent | b1b84b22d16894e5ea2bc7d677eb83c011cb6964 (diff) | |
| parent | d5bf8e1275ae1cc79ddb7048d2015160bdf2bddc (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 920105a9..d61d653d 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1375,10 +1375,19 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Mul:
opString = "*"; break;
case BinaryExpr.ResolvedOpcode.Div:
- opString = "/"; break;
+ wr.Write("Dafny.Helpers.EuclideanDivision(");
+ TrParenExpr(e.E0);
+ wr.Write(", ");
+ TrExpr(e.E1);
+ wr.Write(")");
+ break;
case BinaryExpr.ResolvedOpcode.Mod:
- opString = "%"; break;
-
+ wr.Write("Dafny.Helpers.EuclideanModulus(");
+ TrParenExpr(e.E0);
+ wr.Write(", ");
+ TrExpr(e.E1);
+ wr.Write(")");
+ break;
case BinaryExpr.ResolvedOpcode.SetEq:
case BinaryExpr.ResolvedOpcode.SeqEq:
callString = "Equals"; break;
|