diff options
| author |  rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
| commit | e51b347511f11ea1bda810b843e5d61fdf088832 (patch) | |
| tree | d8623e08a29be5c38f198462a2f38d1f41436413 /Source/Dafny | |
| parent | 4453e362a1ed8449f9031454467cd67da5674451 (diff) | |
Dafny:
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Translator.ssc | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index eea9d91b..092ee146 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1303,7 +1303,8 @@ namespace Microsoft.Dafny { substMap.Add(p, ie);
locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(e.Args[i]));
+ Expression ee = e.Args[i];
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), (!)ee.Type, p.Type));
builder.Add(cmd);
}
// check that the preconditions for the call hold
|