diff options
author | 2011-11-09 14:35:54 -0800 | |
---|---|---|
committer | 2011-11-09 14:35:54 -0800 | |
commit | acd54f7fca4b35dfc516906f95daf7916e8d4b0d (patch) | |
tree | abcba86700393098c20f1f46abbc932ef0f111f4 | |
parent | 688d3b7d65a7bd9bb3b49d464bee0cfccf17e12a (diff) |
copied all attributes of the constructor (except for :constructor) to the selector and membership functions
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index b5c45943..8542ad01 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -152,11 +152,19 @@ namespace Microsoft.Boogie { Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);
Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);
selector.AddAttribute("selector");
+ for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {
+ if (kv.Key == "constructor") continue;
+ selector.AddAttribute(kv.Key, kv.Params.ToArray());
+ }
program.TopLevelDeclarations.Add(selector);
}
Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);
Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);
Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);
+ for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {
+ if (kv.Key == "constructor") continue;
+ isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());
+ }
isConstructor.AddAttribute("membership");
program.TopLevelDeclarations.Add(isConstructor);
}
|