Merge branch 'master' into lean-auto-classical

Author: atomb

.github/workflows/test-lean-auto.yml

@@ -17,7 +17,7 @@ jobs:
       - name: Setup dotnet
         uses: actions/setup-dotnet@v3
         with:
-          dotnet-version: '6.0.x'
+          dotnet-version: '8.0.x'
       - name: Setup Z3
         uses: cda-tum/setup-z3@v1
         with:

.github/workflows/test.yml

@@ -24,9 +24,9 @@ jobs:
         lit_param: ["batch_mode=True", "batch_mode=False"]
     steps:
       - name: Setup dotnet
-        uses: actions/setup-dotnet@v3
+        uses: actions/setup-dotnet@v4
         with:
-          dotnet-version: '6.0.x'
+          dotnet-version: '8.0.x'
       - name: Checkout Boogie
         uses: actions/checkout@v3
         with:

README.md

@@ -20,22 +20,19 @@ input, optionally infers some invariants in the given Boogie program, and then
 generates verification conditions that are passed to an SMT solver. The default
 SMT solver is [Z3](https://github.com/Z3Prover/z3).
 
+A tutorial for Boogie is available [here](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf).
+The documentation in this tutorial, although slightly out-of-date, captures the essence of the Boogie language and tool.
+
 Boogie has long been used for modeling and verifying sequential programs.
 Recently, through its [Civl](https://civl-verifier.github.io/) extension, Boogie 
 has become capable of modeling concurrent and distributed systems.
 
-## Documentation
-
-Here are some resources to learn more about Boogie. Be aware that some
-information might be incomplete or outdated.
-
-* [Documentation](https://boogie-docs.readthedocs.org/en/latest/)
-* [Language reference](https://boogie-docs.readthedocs.org/en/latest/LangRef.html).
-
-## Getting help and contribute
+## Getting help
 
 You can ask questions and report issues on our [issue tracker](https://github.com/boogie-org/boogie/issues).
 
+## Contribute
+
 We are happy to receive contributions via [pull requests](https://github.com/boogie-org/boogie/pulls).
 
 ## Dependencies

Source/AbstractInterpretation/Traverse.cs

@@ -18,44 +18,44 @@ public class WidenPoints
     public static void Compute(Program program)
     {
       Contract.Requires(program != null);
-      cce.BeginExpose(program);
+      Cce.BeginExpose(program);
 
       foreach (var impl in program.Implementations)
       {
         if (impl.Blocks != null && impl.Blocks.Count > 0)
         {
-          Contract.Assume(cce.IsConsistent(impl));
-          cce.BeginExpose(impl);
+          Contract.Assume(Cce.IsConsistent(impl));
+          Cce.BeginExpose(impl);
           Block start = impl.Blocks[0];
           Contract.Assume(start != null);
-          Contract.Assume(cce.IsConsistent(start));
+          Contract.Assume(Cce.IsConsistent(start));
           Visit(start);
 
           // We reset the state...
           foreach (Block b in impl.Blocks)
           {
-            cce.BeginExpose(b);
+            Cce.BeginExpose(b);
             b.TraversingStatus = Block.VisitState.ToVisit;
-            cce.EndExpose();
+            Cce.EndExpose();
           }
 
-          cce.EndExpose();
+          Cce.EndExpose();
         }
       }
 
-      cce.EndExpose();
+      Cce.EndExpose();
     }
 
     static void Visit(Block b)
     {
       Contract.Requires(b != null);
-      Contract.Assume(cce.IsExposable(b));
+      Contract.Assume(Cce.IsExposable(b));
       if (b.TraversingStatus == Block.VisitState.BeingVisited)
       {
-        cce.BeginExpose(b);
+        Cce.BeginExpose(b);
         // we got here through a back-edge
         b.WidenBlock = true;
-        cce.EndExpose();
+        Cce.EndExpose();
       }
       else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
       {
@@ -66,15 +66,15 @@ static void Visit(Block b)
         Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);
 
         GotoCmd g = (GotoCmd) b.TransferCmd;
-        cce.BeginExpose(b);
+        Cce.BeginExpose(b);
 
-        cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
+        Cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
         b.TraversingStatus = Block.VisitState.BeingVisited;
 
         // labelTargets is made non-null by Resolve, which we assume
         // has already called in a prior pass.
         Contract.Assume(g.LabelTargets != null);
-        cce.BeginExpose(g.LabelTargets);
+        Cce.BeginExpose(g.LabelTargets);
         foreach (Block succ in g.LabelTargets)
           //              invariant b.currentlyTraversed;
           //PM: The following loop invariant will work once properties are axiomatized
@@ -84,7 +84,7 @@ static void Visit(Block b)
           Visit(succ);
         }
 
-        cce.EndExpose();
+        Cce.EndExpose();
 
         Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);
         //            System.Diagnostics.Debug.Assert(b.currentlyTraversed);
@@ -94,7 +94,7 @@ static void Visit(Block b)
         //PM: The folowing assumption is needed because we cannot prove that a simple field update
         //PM: leaves the value of a property unchanged.
         Contract.Assume(g.LabelNames == null || g.LabelNames.Count == g.LabelTargets.Count);
-        cce.EndExpose();
+        Cce.EndExpose();
       }
       else
       {
@@ -113,13 +113,13 @@ public static List<Block> ComputeLoopBodyFrom(Block block)
     {
       Contract.Requires(block.WidenBlock);
       Contract.Requires(block != null);
-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+      Contract.Ensures(Cce.NonNullElements(Contract.Result<List<Block>>()));
 
       Contract.Assert(rootBlock == null);
       rootBlock = block;
 
-      List<Block /*!*/> blocksInLoop = new List<Block /*!*/>(); // We use a list just because .net does not define a set
-      List<Block /*!*/> visitingPath = new List<Block /*!*/>(); // The order is important, as we want paths
+      List<Block> blocksInLoop = new List<Block>(); // We use a list just because .net does not define a set
+      List<Block> visitingPath = new List<Block>(); // The order is important, as we want paths
 
       blocksInLoop.Add(block);
 
@@ -141,8 +141,8 @@ public static List<Block> ComputeLoopBodyFrom(Block block)
     private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath)
     {
       Contract.Requires(block != null);
-      Contract.Requires(cce.NonNullElements(path));
-      Contract.Requires(cce.NonNullElements(path));
+      Contract.Requires(Cce.NonNullElements(path));
+      Contract.Requires(Cce.NonNullElements(path));
 
       #region case 1. We visit the root => We are done, "path" is a path inside the loop
 

Source/BaseTypes/BigDec.cs

@@ -153,7 +153,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());

Source/BaseTypes/BigFloat.cs

@@ -213,7 +213,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       if (value == "")

Source/BaseTypes/BigNum.cs

@@ -145,10 +145,10 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
-      return cce.NonNull(val.ToString());
+      return Cce.NonNull(val.ToString());
     }
 
     //////////////////////////////////////////////////////////////////////////////
@@ -158,7 +158,7 @@ public override int GetHashCode()
     // int32.ToString(format) does) 
 
     [Pure]
-    public string /*!*/ ToString(string /*!*/ format)
+    public string ToString(string format)
     {
       Contract.Requires(format != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -185,7 +185,7 @@ public override int GetHashCode()
     private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
 
     [Pure]
-    private string /*!*/ toHex(string /*!*/ format)
+    private string toHex(string format)
     {
       Contract.Requires(format != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -202,7 +202,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    private int extractPrecision(string /*!*/ format)
+    private int extractPrecision(string format)
     {
       Contract.Requires(format != null);
       if (format.Length > 1)
@@ -216,7 +216,7 @@ private int extractPrecision(string /*!*/ format)
     }
 
     [Pure]
-    private string /*!*/ addMinus(int signum, string /*!*/ suffix)
+    private string addMinus(int signum, string suffix)
     {
       Contract.Requires(suffix != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -229,7 +229,7 @@ private int extractPrecision(string /*!*/ format)
     }
 
     [Pure]
-    private string /*!*/ prefixWithZeros(int minLength, string /*!*/ suffix)
+    private string prefixWithZeros(int minLength, string suffix)
     {
       Contract.Requires(suffix != null);
       Contract.Ensures(Contract.Result<string>() != null);

Source/BaseTypes/Rational.cs

@@ -129,7 +129,7 @@ public BigNum Denominator
       get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; }
     }
 
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return String.Format("{0}/{1}", Numerator, Denominator);

Source/BaseTypes/RoundingMode.cs

@@ -67,7 +67,7 @@ public override int GetHashCode()
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       return val;

Source/BaseTypes/Set.cs

@@ -30,7 +30,7 @@ public GSet()
       //:base();
     }
 
-    private GSet(Dictionary<T, int> /*!*/ ht, List<T> arr)
+    private GSet(Dictionary<T, int> ht, List<T> arr)
     {
       Contract.Requires(ht != null);
       Contract.Requires(arr != null);
@@ -47,7 +47,7 @@ public GSet(int capacity)
     }
 
 
-    public readonly static GSet<T> /*!*/
+    public readonly static GSet<T>
       Empty = new GSet<T>();
 
     public void Clear()
@@ -146,7 +146,7 @@ public T Take()
       return r;
     }
 
-    public void Intersect(GSet<T> /*!*/ s)
+    public void Intersect(GSet<T> s)
     {
       Contract.Requires(s != null);
       if (s == this)
@@ -222,7 +222,7 @@ public bool ContainsRange(IEnumerable<T> s)
       return true;
     }
 
-    public object /*!*/ Clone()
+    public object Clone()
     {
       Contract.Ensures(Contract.Result<object>() != null);
       return new GSet<T>(new Dictionary<T, int>(ht), new List<T>(arr));
@@ -234,11 +234,11 @@ public virtual int Count
     }
 
     [Pure]
-    public override string /*!*/ ToString()
+    public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
       string s = null;
-      foreach (object /*!*/ key in ht.Keys)
+      foreach (object key in ht.Keys)
       {
         Contract.Assert(key != null);
         if (s == null)
@@ -266,34 +266,33 @@ public virtual int Count
     //----------------------------- Static Methods ---------------------------------
 
     // Functional Intersect
-    public static GSet<T> /*!*/ Intersect(GSet<T> /*!*/ a, GSet<T> /*!*/ b)
+    public static GSet<T> Intersect(GSet<T> a, GSet<T> b)
     {
       Contract.Requires(b != null);
       Contract.Requires(a != null);
       Contract.Ensures(Contract.Result<GSet<T>>() != null);
-      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
-      GSet<T> /*!*/
-        res = (GSet<T> /*!*/) cce.NonNull(a.Clone());
+      GSet<T>
+        res = (GSet<T>) Cce.NonNull(a.Clone());
       res.Intersect(b);
       return res;
     }
 
     // Functional Union
-    public static GSet<T> /*!*/ Union(GSet<T> /*!*/ a, GSet<T> /*!*/ b)
+    public static GSet<T> Union(GSet<T> a, GSet<T> b)
     {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
       Contract.Ensures(Contract.Result<GSet<T>>() != null);
       //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
-      GSet<T> /*!*/
-        res = (GSet<T> /*!*/) cce.NonNull(a.Clone());
+      GSet<T>
+        res = (GSet<T>) Cce.NonNull(a.Clone());
       res.AddRange(b);
       return res;
     }
 
-    public delegate bool SetFilter(object /*!*/ obj);
+    public delegate bool SetFilter(object obj);
 
-    public static GSet<T> /*!*/ Filter(GSet<T> /*!*/ a, Func<T, bool> filter)
+    public static GSet<T> Filter(GSet<T> a, Func<T, bool> filter)
     {
       Contract.Requires(filter != null);
       Contract.Requires(a != null);