summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-09 15:46:37 +0000
committerGravatar tabarbe <unknown>2010-08-09 15:46:37 +0000
commit378caef76d846b8a587de40d75ff0c903af095c3 (patch)
tree496fc03f5db5a33e092e52c78572991c4f0736d8 /Source/VCGeneration
parente308fe8b4ea5e3a698ac0c843d388f95d32d3bde (diff)
Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/cce.cs6
1 files changed, 4 insertions, 2 deletions
diff --git a/Source/VCGeneration/cce.cs b/Source/VCGeneration/cce.cs
index 34749b5f..f97ffd96 100644
--- a/Source/VCGeneration/cce.cs
+++ b/Source/VCGeneration/cce.cs
@@ -1,4 +1,5 @@
-using System;
+#if CONTRACTS_FULL
+using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Text;
@@ -101,4 +102,5 @@ public class ReadsAttribute : System.Attribute {
};
public ReadsAttribute(object o) {
}
-} \ No newline at end of file
+}
+#endif \ No newline at end of file