diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-07-11 19:09:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-07-11 19:09:41 -0700 |
| commit | 1dd0047d2bb46b64a4d04259ba7803fc09898194 (patch) | |
| tree | 554bf9b30251a62c258a221343936f25e17cd51a /Dafny | |
| parent | eacaf0b44276f0a61d6cc4204bb4d48d02fc0548 (diff) | |
| parent | 61acaf623c5acf36b57d958e788f10f3c23bd309 (diff) | |
Merge
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Compiler.cs | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 920105a9..d61d653d 100644 --- a/Dafny/Compiler.cs +++ b/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;
|