summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2011-12-07 09:54:01 +0100
committerGravatar wuestholz <unknown>2011-12-07 09:54:01 +0100
commit5c2205250c6f141cf61fdec89929d93b78e8472c (patch)
tree96c63703a5e999ea55c8581c1f1416f7ad88ac01 /Source/Dafny
parente104999ceabc9420a300771b585df7e643312bf3 (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.cs2
-rw-r--r--Source/Dafny/DafnyAst.cs4
-rw-r--r--Source/Dafny/Translator.cs2
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);