Boogie: Committing my port of the SMTLib project

1 files changed, 55 insertions, 28 deletions

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 08c0e6a3..a0d56601 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -7,7 +7,7 @@ using System;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Boogie.VCExprAST;

 

 namespace Microsoft.Boogie.SMTLib

@@ -17,68 +17,93 @@ namespace Microsoft.Boogie.SMTLib
 

   public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

 

-    private readonly UniqueNamer! Namer;

+    private readonly UniqueNamer Namer;

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(Namer!=null);

+      Contract.Invariant(AllDecls != null);

+      Contract.Invariant(IncDecls != null);

+      Contract.Invariant(KnownFunctions != null);

+      Contract.Invariant(KnownVariables != null);

+}

+

 

-    public TypeDeclCollector(UniqueNamer! namer) {

+    public TypeDeclCollector(UniqueNamer namer) {

+      Contract.Requires(namer != null);

       this.Namer = namer;

     }

 

     // not used

-    protected override bool StandardResult(VCExpr! node, bool arg) {

+    protected override bool StandardResult(VCExpr node, bool arg) {

+      Contract.Requires(node != null);

       return true;

     }

 

-    private readonly List<string!>! AllDecls = new List<string!> ();

-    private readonly List<string!>! IncDecls = new List<string!> ();

+    private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();

+    private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();

+

+    private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions =

+      new Dictionary<Function/*!*/, bool> ();

+    private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

+      new Dictionary<VCExprVar/*!*/, bool> ();

 

-    private readonly IDictionary<Function!, bool>! KnownFunctions =

-      new Dictionary<Function!, bool> ();

-    private readonly IDictionary<VCExprVar!, bool>! KnownVariables =

-      new Dictionary<VCExprVar!, bool> ();

+    public List<string/*!>!*/> AllDeclarations { get {

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));

 

-    public List<string!>! AllDeclarations { get {

-      List<string!>! res = new List<string!> ();

+      List<string>/*!>!*/ res = new List<string/*!*/> ();

       res.AddRange(AllDecls);

       return res;

     } }

 

-    public List<string!>! GetNewDeclarations() {

-      List<string!>! res = new List<string!> ();

+    public List<string/*!>!*/> GetNewDeclarations() {

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));

+      List<string>/*!>!*/ res = new List<string/*!*/>();

       res.AddRange(IncDecls);

       IncDecls.Clear();

       return res;

     }

 

-    private void AddDeclaration(string! decl) {

+    private void AddDeclaration(string decl) {

+      Contract.Requires(decl != null);

       AllDecls.Add(decl);

       IncDecls.Add(decl);

     }

 

-    public void Collect(VCExpr! expr) {

+    public void Collect(VCExpr expr) {

+      Contract.Requires(expr != null);

       Traverse(expr, true);

     }

 

     ///////////////////////////////////////////////////////////////////////////

 

-    private static string! TypeToString(Type! t) {

+    private static string TypeToString(Type t) {

+      Contract.Requires(t != null);

+      Contract.Ensures(Contract.Result<string>() != null);

+

       return SMTLibExprLineariser.TypeToString(t);

     }

 

-    public override bool Visit(VCExprNAry! node, bool arg) {

+    public override bool Visit(VCExprNAry node, bool arg) {

+      Contract.Requires(node != null);

       // there are a couple of cases where operators have to be

       // registered by generating appropriate statements

 

       VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

       if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

-        Function! f = op.Func;

-        string! printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));

-        string! decl = ":extrafuns ((" + printedName;

-

-        foreach (Variable! v in f.InParams) {

+        Function f = op.Func;

+        Contract.Assert(f!=null);

+        string printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));

+        Contract.Assert(printedName!=null);

+        string decl = ":extrafuns ((" + printedName;

+

+        foreach (Variable v in f.InParams) {

+          Contract.Assert(v!=null);

           decl += " " + TypeToString(v.TypedIdent.Type);

         }

-        assert f.OutParams.Length == 1;

-        foreach (Variable! v in f.OutParams) {

+       Contract.Assert(f.OutParams.Length == 1);

+        foreach (Variable v in f.OutParams) {

+          Contract.Assert(v!=null);

           decl += " " + TypeToString(v.TypedIdent.Type);

         }

 

@@ -91,10 +116,12 @@ namespace Microsoft.Boogie.SMTLib
       return base.Visit(node, arg);

     }

 

-    public override bool Visit(VCExprVar! node, bool arg) {

+    public override bool Visit(VCExprVar node, bool arg) {

+      Contract.Requires(node != null);

       if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {

-        string! printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name));

-        string! decl =

+        string printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name));

+        Contract.Assert(printedName!=null);

+        string decl =

           ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";

         AddDeclaration(decl);

         KnownVariables.Add(node, true);