diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-10-05 19:31:21 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-10-05 19:31:21 -0700 |
| commit | 7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 (patch) | |
| tree | 39253d3c9014af50b1ec1d0eedb7ebd720ddbd2f /Source/BoogieDriver | |
| parent | 696796e1dcea137ee9b5c270b233892dd3267155 (diff) | |
added membership tests
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 1 |
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);
}
}
|