diff options
| author |  Jason Koenig <unknown> | 2011-07-08 14:18:37 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-08 14:18:37 -0700 |
| commit | 2955170d9183a7bb8598ce89a61818623f321f16 (patch) | |
| tree | 1e33a0ea962eb43d1f097cd71f93eb387a363343 /Dafny/Compiler.cs | |
| parent | 87e454054629237ce9b2dcf2a31de059bbda1749 (diff) | |
Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)
Diffstat (limited to 'Dafny/Compiler.cs')
| -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;
|