summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyQuant.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-02-10 18:14:46 -0800
committerGravatar Rustan Leino <unknown>2014-02-10 18:14:46 -0800
commit8567d68f7f04f87b2d4270e18713bdcdf4d26031 (patch)
tree75e633b53ac24d35c2d8d51641736a6b6e22ac99 /Source/Core/AbsyQuant.cs
parente2feccce72c3f6b6d7ef0ab6c82675e1ff86a5f1 (diff)
Fixed errors in the use of Code Contracts
Diffstat (limited to 'Source/Core/AbsyQuant.cs')
-rw-r--r--Source/Core/AbsyQuant.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 06d72ee9..e2bbcdf5 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -271,6 +271,7 @@ namespace Microsoft.Boogie {
current.Next = other;
}
// Look for {:name string} in list of attributes.
+ [Pure]
public static string FindStringAttribute(QKeyValue kv, string name) {
Contract.Requires(name != null);
for (; kv != null; kv = kv.Next) {