* Added "deprecated" comment in help message about /interprocInfer switch. The functionality is currently broken.

* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it)
* Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods

6 files changed, 29 insertions, 28 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 18d29c73..35175881 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -15,17 +15,19 @@ namespace Microsoft.Boogie.AbstractInterpretation
 

   public class CallSite

   {

-    public Implementation! Impl;

-    public Block! Block;

-    public int Statement; // invariant: Block[Statement] is CallCmd

-    public AI.Lattice.Element! KnownBeforeCall;

+    public readonly Implementation! Impl;

+    public readonly Block! Block;

+    public readonly int Statement; // invariant: Block[Statement] is CallCmd

+    public readonly AI.Lattice.Element! KnownBeforeCall;

+    public readonly ProcedureSummaryEntry! SummaryEntry;

 

-    public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e)

+    public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e, ProcedureSummaryEntry! summaryEntry)

     {

       this.Impl = impl;

       this.Block = b;

       this.Statement = stmt;

       this.KnownBeforeCall = e;

+      this.SummaryEntry = summaryEntry;

     }

   }

 

@@ -532,7 +534,7 @@ namespace Microsoft.Boogie
       this.name = name;

       // base(tok);

     }

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString()

     {

       return (!) Name;

@@ -775,7 +777,7 @@ namespace Microsoft.Boogie
       TypecheckAttributes(tc);

       this.TypedIdent.Typecheck(tc);

     }

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public object DoVisit(AI.ExprVisitor! visitor)

     {

       return visitor.VisitVariable(this);

@@ -1496,8 +1498,6 @@ namespace Microsoft.Boogie
     [Rep]

     public readonly ProcedureSummary! Summary;

 

-    public static bool ShowSummaries = false;

-

     public Procedure (

       IToken! tok, 

       string! name, 

@@ -1559,9 +1559,9 @@ namespace Microsoft.Boogie
         e.Emit(stream, level);

       }

 

-      if (ShowSummaries)

+      if (!CommandLineOptions.Clo.IntraproceduralInfer)

       {

-        for (int s=0; s<this.Summary.Count; s++)

+        for (int s=0; s < this.Summary.Count; s++)

         {

           ProcedureSummaryEntry! entry = (!) this.Summary[s];

           stream.Write(level + 1, "// ");

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index d0c65c96..da4f4247 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -775,7 +775,7 @@ namespace Microsoft.Boogie
       this.PostInvariant = null;

     }

 

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString()

     {

       return this.Label + (this.widenBlock? "[w]" : "");

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 2dd85a65..bed34c63 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -1842,7 +1842,8 @@ namespace Microsoft.Boogie
                    switch on its left

   /checkInfer    : instrument inferred invariants as asserts to be checked by

                    theorem prover

-  /interprocInfer : perform interprocedural inference

+  /interprocInfer : perform interprocedural inference (deprecated, not

+                    supported)

   /contractInfer : perform procedure contract inference

   /logInfer      : print debug output during inference

   /printInstrumented : print Boogie program after it has been

diff --git a/Source/Core/GraphAlgorithms.ssc b/Source/Core/GraphAlgorithms.ssc
index 7ce07d6e..aac45d73 100644
--- a/Source/Core/GraphAlgorithms.ssc
+++ b/Source/Core/GraphAlgorithms.ssc
@@ -33,7 +33,7 @@ namespace Microsoft.Boogie
     public bool IsReadOnly { get { return nodesMap.IsReadOnly; } }

     public void Add(Node item) { nodesMap.Add(item,null); }

     public void Clear() { nodesMap.Clear(); }

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public bool Contains(Node item) { return nodesMap.ContainsKey(item); }

     public void CopyTo(Node[]! array, int arrayIndex) { nodes.CopyTo(array, arrayIndex); }

     public bool Remove(Node item) { return nodesMap.Remove(item); }

@@ -148,7 +148,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString()

     {

       string outStr = "";

diff --git a/Source/Core/OOLongUtil.ssc b/Source/Core/OOLongUtil.ssc
index 81dadf1b..e87666f3 100644
--- a/Source/Core/OOLongUtil.ssc
+++ b/Source/Core/OOLongUtil.ssc
@@ -34,7 +34,7 @@ namespace Boogie.Util {
       b.Flush();

     }

 

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString() {

       return "<TeeWriter: " + a.ToString() + ", " + b.ToString() + ">";

     }

diff --git a/Source/Core/PureCollections.ssc b/Source/Core/PureCollections.ssc
index d51ebe62..971af388 100644
--- a/Source/Core/PureCollections.ssc
+++ b/Source/Core/PureCollections.ssc
@@ -80,7 +80,7 @@ namespace PureCollections {
     [Pure][Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

     public static bool operator != (Tuple s, Tuple t) { return ! (t == s); }

 

-    [Pure][Reads(ReadsAttribute.Reads.Owned)] 

+    [Pure]

     public override int GetHashCode (){

       int h =0;

       assume this.elems != null;

@@ -120,7 +120,7 @@ namespace PureCollections {
     }

     

     //ToString - - - -  - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString() {

       assert this.elems != null; 

       if (elems.Length==0)

@@ -165,7 +165,7 @@ namespace PureCollections {
       } while (index < map.elems.Length && map.elems[index] == null);

       return index < map.elems.Length;

     }

-    public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}

+    public object Current{ get { assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}

     public void Reset() {index = -1; }

   }

   

@@ -281,7 +281,7 @@ namespace PureCollections {
     }

 

     //ToString - - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString() {

       if (card ==0)

         return "{|->}";

@@ -351,7 +351,7 @@ namespace PureCollections {
     public static bool operator != (Map s, Map t){ 

       return ! (t == s); 

     }

-    [Pure][Reads(ReadsAttribute.Reads.Owned)] 

+    [Pure]

     public override int GetHashCode (){

       int h =0;

       assert this.elems != null;

@@ -368,7 +368,7 @@ namespace PureCollections {
  

     //Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - - 

    

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public bool Has(Object x) {      

       if (x == null) 

         throw new MissingCase();      

@@ -427,7 +427,7 @@ namespace PureCollections {
       //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);

       return index < seq.Length;

     }

-    public object Current{ [Pure][Reads(ReadsAttribute.Reads.Owned)] get {assert seq.elems != null; return seq.elems[index]; }}

+    public object Current{ get { assert seq.elems != null; return seq.elems[index]; }}

     public void Reset() {index = -1; }

   }

   

@@ -546,7 +546,7 @@ namespace PureCollections {
     }

 

     //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public override string! ToString() {

       string s ="";

       assert this.elems != null; 

@@ -596,7 +596,7 @@ namespace PureCollections {
     public static bool operator != (Sequence s, Sequence t){ 

       return !(s == t); 

     }

-    [Pure][Reads(ReadsAttribute.Reads.Owned)] 

+    [Pure]

     public override int GetHashCode (){

       int h = 0;

       for(int i = 0; i < card; i++)

@@ -645,7 +645,7 @@ namespace PureCollections {
     public static bool operator >= (Sequence s, Sequence t){ return t <= s;}

 

     //pure---------------------------------------------------------------

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public bool Has(object x) {         // WS translate to tailrecursion 

       if (x == null)

         throw new MissingCase();

@@ -658,7 +658,7 @@ namespace PureCollections {
 

     // the index of the first occurrence of x in this sequence,

     // or -1 if x does not occur

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public int IndexOf(object x) {

       if (x == null)

         throw new MissingCase();

@@ -671,7 +671,7 @@ namespace PureCollections {
 

     // the index of the last occurrence of x in this sequence,

     // or -1 if x does not occur

-    [Pure][Reads(ReadsAttribute.Reads.Owned)]

+    [Pure]

     public int LastIndexOf(object x) {

       if (x == null)

         throw new MissingCase();