From 4c81e90e18b1d142c50453470fe9647693ef8de4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 6 Jan 2016 19:00:18 -0800
Subject: Removed Contract.Requires from method overrides (preconditions of
 overrides are inherited from the overridden method and Code Contracts will
 copy those preconditions to make sure the right run-time checking happens;
 when Code Contracts finds preconditions on overrides, it emits warnings).

---
 Source/Dafny/Rewriter.cs                      | 1 -
 Source/Dafny/Triggers/QuantifierSplitter.cs   | 1 -
 Source/Dafny/Triggers/QuantifiersCollector.cs | 1 -
 3 files changed, 3 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 13b16066..2e18c4e6 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -89,7 +89,6 @@ namespace Microsoft.Dafny
     internal class ForAllStmtVisitor : TopDownVisitor<bool>
     {
       protected override bool VisitOneStmt(Statement stmt, ref bool st) {
-        Contract.Requires(stmt != null);
         if (stmt is ForallStmt) {
           ForallStmt s = (ForallStmt)stmt;
           if (s.Kind == ForallStmt.ParBodyKind.Proof) {
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index e46b64fb..d0b2b430 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -115,7 +115,6 @@ namespace Microsoft.Dafny.Triggers {
     }
 
     protected override void VisitOneStmt(Statement stmt) {
-      Contract.Requires(stmt != null);
       if (stmt is ForallStmt) {
         ForallStmt s = (ForallStmt)stmt;
         if (s.ForallExpressions != null) {
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index 789e7614..b887435b 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -42,7 +42,6 @@ namespace Microsoft.Dafny.Triggers {
     }
 
     protected override bool VisitOneStmt(Statement stmt, ref bool st) {
-      Contract.Requires(stmt != null);
       if (stmt is ForallStmt) {
         ForallStmt s = (ForallStmt)stmt;
         if (s.ForallExpressions != null) {
-- 
cgit v1.2.3