Boogie:

* Bug fix:  Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case)
* Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants.  Previously, the only option was to instrument at the beginning and end of every basic block.  The new option, which is now the default, is to instrument only at the beginning of loop heads.
* Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized
* Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1

Boogie refactoring:
* Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand
* Cleaned up some parsing of command-line options

1 files changed, 0 insertions, 229 deletions

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index baf12310..eaf4e640 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -836,8 +836,6 @@ namespace Microsoft.Boogie
     

     T Visit(FunctionCall! functionCall);

     

-    T Visit(LoopPredicateName! loopPredicateName);

-    

     T Visit(MapSelect! mapSelect);

     

     T Visit(MapStore! mapStore);

@@ -1572,171 +1570,6 @@ namespace Microsoft.Boogie
 

   }

 

-  /// <summary>

-  /// A subclass of FunctionCall that stands for a zero-argument function call, used as a loop invariant placeholder

-  /// </summary>

-  public class LoopPredicateName : FunctionCall

-  {         

-    private Block! block;             // The block the predicate refers to    

-    public Block! Block

-    {    

-      get                       

-      {

-        return block;

-      }

-    }

-

-    private string! blockName;      // The name of the block

-    private ICollection<Block!>! component;

-    public ICollection<Block!>! Component

-    { 

-      get

-      {

-        return this.component;

-      }

-    }

-

-    public string! Name 

-    {

-      get

-      {

-        return "J_" + this.blockName;

-      }

-    } 

-

-    invariant block.Label == blockName;   // Note that we ask for object equality of strings...

-

-    private Hashtable /* Var -> Incarnations */ preHavocIncarnationMap;

-    public Hashtable PreHavocIncarnationMap

-    {

-      get 

-      {

-        return this.preHavocIncarnationMap;

-      }

-    }

-

-    private Hashtable /* Var -> Incarnations */ postHavocIncarnationMap;

-    public Hashtable PostHavocIncarnationMap

-    {

-      get 

-      {

-        return this.postHavocIncarnationMap;

-      }

-    }

-

-

-    // Those below are the inverse maps of the maps between variables and incarnations

-    private Hashtable /* String -> Var */ preHavocIncarnationInverseMap;

-    private Hashtable /* String -> Var */ postHavocIncarnationInverseMap;

-

-    public Hashtable PreHavocInverseMap 

-    {

-      get 

-      {

-        if(this.preHavocIncarnationInverseMap == null) 

-        {

-          this.preHavocIncarnationInverseMap = new Hashtable();

-          assert this.preHavocIncarnationMap != null;                   // If we get at this point, then something is wrong with the program

-          foreach(object! key in (!) (this.preHavocIncarnationMap).Keys) 

-          {

-            object! val = (!) this.preHavocIncarnationMap[key];

-            if(!this.preHavocIncarnationInverseMap.ContainsKey(val.ToString()))

-              this.preHavocIncarnationInverseMap.Add(val.ToString(), key);

-          }

-        }

-        return this.preHavocIncarnationInverseMap;

-      }

-    }

-

-    public Hashtable PostHavocInverseMap 

-    {

-      get 

-      {

-        if(this.postHavocIncarnationInverseMap == null) 

-        {

-          this.postHavocIncarnationInverseMap = new Hashtable();

-          assert this.postHavocIncarnationMap != null;        // If it is null, something is wrong before...

-          foreach(object! key in (!) (this.postHavocIncarnationMap).Keys) 

-          {

-            object! val = (!) this.postHavocIncarnationMap[key];

-            if(!this.postHavocIncarnationInverseMap.ContainsKey(val.ToString()))

-            this.postHavocIncarnationInverseMap.Add(val.ToString(), key);

-          }

-        }

-        return this.postHavocIncarnationInverseMap;

-      }

-    }

-

-    /// <summary>

-    /// Create a new LoopPredicate

-    /// </summary>      

-    public LoopPredicateName(Block! block, ICollection<Block!>! component) 

-      : base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool))

-    {

-      this.block = block;

-      this.blockName = block.Label;

-      this.component = component;

-      // base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool));

-    }       

-

-    public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post) 

-    {

-      assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null;

-        

-      this.preHavocIncarnationMap = pre;

-      this.postHavocIncarnationMap = post;

-    }

-

-    /// <summary>

-    /// Writes down the loop predicate and the incarnations map before and after the havoc statements

-    /// </summary>

-    public override void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext) 

-    {

-      string! pre, post;

-

-      if(this.postHavocIncarnationMap != null && this.preHavocIncarnationMap != null)        

-      {

-        pre = "pre: [ " + hashtableToString(this.preHavocIncarnationMap) +" ]";  

-        post = "post: [ " + hashtableToString(this.postHavocIncarnationMap) +" ]";        

-      }

-      else 

-      {

-        pre = post = "[]";

-      }

-

-      stream.Write("J_" + this.blockName);

-      stream.Write("(");

-      stream.Write(pre + ", " + post);

-      stream.Write(")");

-    }

-

-    public override Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc) 

-    {

-      tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

-      return Type.Bool;

-    }

-

-    public override int ArgumentCount { get { return 0; } }

-

-    private string! hashtableToString(Hashtable! map) 

-    {

-      string! outVal = "";

-

-      foreach (object! key in map.Keys) 

-      {

-        object val = map[key];

-        outVal += key + " -> " + val + ",";

-      }

-

-      return outVal;

-    }    

-

-    public override T Dispatch<T>(IAppliableVisitor<T>! visitor) {

-      return visitor.Visit(this);

-    }

-

-  }

-

   public class NAryExpr : Expr, AI.IFunApp

   {

     [Additive] [Peer]

@@ -1870,68 +1703,6 @@ namespace Microsoft.Boogie
     }

   }

 

-  /// <summary>

-  /// An instance of LoopPredicate stands for a loop invariant predicate 

-  /// </summary>

-  public class LoopPredicate : NAryExpr 

-  {

-    private static ExprSeq! emptyArgs = new ExprSeq(new Expr[0]);         // Share the emptylist of arguments among several instances

-    

-    invariant loopPredicateName == Fun;                                   // loopPredicateName is just a way of subtyping Fun...

-    LoopPredicateName! loopPredicateName; 

-

-    Hashtable /* Var -> Expr */ preHavocIncarnationMap;

-    Hashtable /* Var -> Expr */ postHavocIncarnationMap;    

-

-    private Block! block;                         // The block the predicate refers to

-    private string! BlockName;                    // Name of the widen block the predicate refers to 

-    private ICollection<Block!> component;        // The component the block belongs to 

-    

-    /// <summary>

-    /// Create a predicate (standing for a loop invariant). The parameter are the name of the block and the (strong) connect components the block belongs to

-    /// </summary>

-    public LoopPredicate(Block! block, ICollection<Block!>! component) 

-    {

-      this.block = block;

-      this.BlockName = block.Label;

-      this.component = component;      

-

-      LoopPredicateName! tmp;        // to please the compiler we introde a temp variable

-      this.loopPredicateName = tmp = new LoopPredicateName(block, component); 

-      base(Token.NoToken, tmp, emptyArgs); // due to locally computed data

-    } 

-

-    public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post) 

-    {

-      assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null; // The method must be called just once

-        

-      this.preHavocIncarnationMap = pre;

-      this.postHavocIncarnationMap = post;

-      this.loopPredicateName.SetPreAndPostHavocIncarnationMaps(pre, post);

-    }  

-

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

-    public override bool Equals(object obj)

-    {

-      if (obj == null) return false;

-      if (!(obj is LoopPredicate)) return false;

-

-      LoopPredicate pred = (LoopPredicate) obj;

-      return this.BlockName.Equals(pred.BlockName);

-    }

-

-    [Pure]

-    public override int GetHashCode() 

-    {

-      return this.BlockName.GetHashCode();

-    }

-

-    public override Absy! StdDispatch(StandardVisitor! visitor)

-    {

-      return visitor.VisitLoopPredicate(this);

-    }

-  }

-

   public class MapSelect : IAppliable, AI.IFunctionSymbol {

 

     public readonly int Arity;