diff options
| author |  wuestholz <unknown> | 2011-09-20 09:59:16 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-09-20 09:59:16 +0200 |
| commit | 609deac438ce403abb679dc89a1ad6c98770e54c (patch) | |
| tree | 2048c351c5db64bb285f1eb6f1afaefdec147a77 /Source | |
| parent | d49d27d02674eb95f35ab0e6728ab8b64e9c5e10 (diff) | |
Dafny: Fixed an assertion violation in the "Checked" configuration.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 |
2 files changed, 3 insertions, 2 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index cbea8535..a9c41efb 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2380,7 +2380,6 @@ namespace Microsoft.Boogie { public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)
: this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {
- Contract.Requires(kv != null);
Contract.Requires(structuredStmts != null);
Contract.Requires(localVariables != null);
Contract.Requires(outParams != null);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a1058786..17df4e06 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1069,9 +1069,11 @@ namespace Microsoft.Dafny { stmts = builder.Collect(m.tok);
}
+ QKeyValue kv = etran.TrAttributes(m.Attributes);
+
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
- localVariables, stmts, etran.TrAttributes(m.Attributes));
+ localVariables, stmts, kv);
sink.TopLevelDeclarations.Add(impl);
currentMethod = null;
|