Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.cs

3 files changed, 12 insertions, 6 deletions

diff --git a/Source/AbsInt/cce.cs b/Source/AbsInt/cce.cs
index c8d7a4ab..8666256e 100644
--- a/Source/AbsInt/cce.cs
+++ b/Source/AbsInt/cce.cs
@@ -1,4 +1,5 @@
-using System;

+#if CONTRACTS_FULL

+using System;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Text;

@@ -59,4 +60,5 @@ public class PeerAttribute : System.Attribute {
 public class RepAttribute : System.Attribute {

 }

 public class CapturedAttribute : System.Attribute {

-}
\ No newline at end of file
+}

+#endif
\ No newline at end of file
diff --git a/Source/BoogieDriver/cce.cs b/Source/BoogieDriver/cce.cs
index 34749b5f..f97ffd96 100644
--- a/Source/BoogieDriver/cce.cs
+++ b/Source/BoogieDriver/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
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