diff options
author | wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
---|---|---|
committer | wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
commit | 5c2205250c6f141cf61fdec89929d93b78e8472c (patch) | |
tree | 96c63703a5e999ea55c8581c1f1416f7ad88ac01 /Source/Dafny | |
parent | e104999ceabc9420a300771b585df7e643312bf3 (diff) |
Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable wellformedness checks).
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 4 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index d0e0cb0e..b49c011f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1367,7 +1367,7 @@ namespace Microsoft.Dafny { Type elType = cce.NonNull((MultiSetType)e.Type).Arg;
wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));
TrExprList(e.Elements);
-
+
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
Type elType = cce.NonNull((SeqType)e.Type).Arg;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8272736c..99ebe8da 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -262,7 +262,7 @@ namespace Microsoft.Dafny { this.Arg = arg;
}
}
-
+
public class SetType : CollectionType {
public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
@@ -2149,7 +2149,7 @@ namespace Microsoft.Dafny { get { return Elements; }
}
}
-
+
public class SetDisplayExpr : DisplayExpression {
public SetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
: base(tok, elements) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index d1e41663..5f382eb6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1499,7 +1499,7 @@ namespace Microsoft.Dafny { Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
req.Add(Requires(f.tok, true, context, null, null));
Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
- req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
+ req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq(), etran.TrAttributes(f.Attributes, null));
sink.TopLevelDeclarations.Add(proc);
VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);
|