summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-10-05 19:31:21 -0700
committerGravatar qadeer <qadeer@microsoft.com>2011-10-05 19:31:21 -0700
commit7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 (patch)
tree39253d3c9014af50b1ec1d0eedb7ebd720ddbd2f /Source/BoogieDriver
parent696796e1dcea137ee9b5c270b233892dd3267155 (diff)
added membership tests
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 722bc99e..b5c45943 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -157,6 +157,7 @@ namespace Microsoft.Boogie {
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);
+ isConstructor.AddAttribute("membership");
program.TopLevelDeclarations.Add(isConstructor);
}
}