From f6f281a60449aea24b257b73cd45fd970afbc57c Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 16 Jul 2010 22:44:33 +0000
Subject: Boogie: I have successfully ported the AbsInt project.  It passes all
 regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed
 AbsInt DLL.

Address any error complaints to t-abarbe@microsoft.com
---
 Source/AbsInt/LoopInvariantsOnDemand.cs | 94 +++++++++++++++++----------------
 1 file changed, 49 insertions(+), 45 deletions(-)

(limited to 'Source/AbsInt/LoopInvariantsOnDemand.cs')

diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs
index 1ebd11b2..49958289 100644
--- a/Source/AbsInt/LoopInvariantsOnDemand.cs
+++ b/Source/AbsInt/LoopInvariantsOnDemand.cs
@@ -3,76 +3,80 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
 //-----------------------------------------------------------------------------
-namespace Microsoft.Boogie.AbstractInterpretation
-{
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using Microsoft.Contracts;
-using AI = Microsoft.AbstractInterpretationFramework;
-using Boogie = Microsoft.Boogie;
+namespace Microsoft.Boogie.AbstractInterpretation {
+  using System;
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics.Contracts;
+  using AI = Microsoft.AbstractInterpretationFramework;
+  using Boogie = Microsoft.Boogie;
+
+
+
   /// <summary>
   /// A visitor of an abstract interpretation expression that collects the free variables 
   /// </summary>      
-  class FreeVariablesVisitor : AI.ExprVisitor 
-  {
-    [Peer] List<AI.IVariable!>! variables;
-    public List<AI.IVariable!>! FreeVariables 
-    {
-      get
-      {
+  class FreeVariablesVisitor : AI.ExprVisitor {
+    [Peer]
+    List<AI.IVariable> variables;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(cce.NonNullElements(variables));
+      Contract.Invariant(cce.NonNullElements(varNames));
+    }
+
+    public List<AI.IVariable> FreeVariables {
+      get {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<AI.IVariable>>()));
+
         return this.variables;
-      }    
+      }
     }
 
-    List<string!>! varNames;    // used to check the consinstency!
+    List<string> varNames;    // used to check the consinstency!
 
-    public FreeVariablesVisitor() 
-    {
-      this.variables = new List<AI.IVariable!>(); 
-      this.varNames = new List<string!>();
+    public FreeVariablesVisitor() {
+      this.variables = new List<AI.IVariable>();
+      this.varNames = new List<string>();
     }
 
-    override public object Default(AI.IExpr! expr)
-    {
-      if (expr is AI.IVariable) 
-      {
-        if(!variables.Contains((AI.IVariable) expr)) 
-        {
-          this.variables.Add((AI.IVariable) expr);
-                      
-          assert ! this.varNames.Contains(expr.ToString());     // If we get there, we have an error: two variables with the same name but different identity  
-             
+    override public object Default(AI.IExpr expr) {
+      Contract.Requires(expr != null);
+      if (expr is AI.IVariable) {
+        if (!variables.Contains((AI.IVariable)expr)) {
+          this.variables.Add((AI.IVariable)expr);
+
+          Contract.Assert(!this.varNames.Contains(expr.ToString()));     // If we get there, we have an error: two variables with the same name but different identity  
+
           this.varNames.Add(expr.ToString());
         }
         return null;
-      }
-      else if (expr is AI.IFunApp)
-        return VisitFunApp((AI.IFunApp) expr);
+      } else if (expr is AI.IFunApp)
+        return VisitFunApp((AI.IFunApp)expr);
       else if (expr is AI.IFunction)
         return VisitFunction((AI.IFunction)expr);
-      else 
-      {
-        assert false;
+      else {
+        Contract.Assert(false);
+        throw new cce.UnreachableException();
       }
     }
 
-    public override object VisitFunApp(AI.IFunApp! funapp)
-    {
-      foreach (AI.IExpr! arg in funapp.Arguments)
-      {
+    public override object VisitFunApp(AI.IFunApp funapp) {
+      Contract.Requires(funapp != null);
+      foreach (AI.IExpr arg in funapp.Arguments) {
+        Contract.Assert(arg != null);
         arg.DoVisit(this);
       }
       return true;
     }
-                
-    public override object VisitFunction(AI.IFunction! fun)
-    {
+
+    public override object VisitFunction(AI.IFunction fun) {
+      Contract.Requires(fun != null);
       fun.Body.DoVisit(this);
       this.variables.Remove(fun.Param);
       return true;
     }
 
-  } 
+  }
 
 }
\ No newline at end of file
-- 
cgit v1.2.3