Cce rename (#998)

.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:

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,7 +113,7 @@ 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;
@@ -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/BigNum.cs

@@ -148,7 +148,7 @@ public override int GetHashCode()
     public override string /*!*/ ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
-      return cce.NonNull(val.ToString());
+      return Cce.NonNull(val.ToString());
     }
 
     //////////////////////////////////////////////////////////////////////////////

Source/BaseTypes/Set.cs

@@ -273,7 +273,7 @@ public virtual int Count
       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());
+        res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
       res.Intersect(b);
       return res;
     }
@@ -286,7 +286,7 @@ public virtual int Count
       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());
+        res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
       res.AddRange(b);
       return res;
     }

Source/BoogieDriver/BoogieDriver.cs

@@ -12,7 +12,7 @@ public class OnlyBoogie
   {
     public static int Main(string[] args)
     {
-      Contract.Requires(cce.NonNullElements(args));
+      Contract.Requires(Cce.NonNullElements(args));
 
       var options = new CommandLineOptions(Console.Out, new ConsolePrinter())
       {

Source/CodeContractsExtender/cce.cs

@@ -6,7 +6,7 @@
 /// <summary>
 /// A class containing static methods to extend the functionality of Code Contracts
 /// </summary>
-public static class cce
+public static class Cce
 {
   //[Pure]
   //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
@@ -29,7 +29,7 @@ public static bool NonNullElements<T>(IEnumerable<T> collection) where T : class
   [Pure]
   public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class
   {
-    return collection != null && cce.NonNullElements(collection.Values);
+    return collection != null && Cce.NonNullElements(collection.Values);
   }
 
   //[Pure]
@@ -46,7 +46,7 @@ public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TV
   [Pure]
   public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) where T : class
   {
-    return (nullability && collection == null) || cce.NonNullElements(collection);
+    return (nullability && collection == null) || Cce.NonNullElements(collection);
     //Should be the same as:
     /*if(nullability&&collection==null)
      * return true;

Source/Concurrency/CivlCoreTypes.cs

@@ -397,7 +397,7 @@ private List<AssertCmd> HoistAsserts(Implementation impl, ConcurrencyOptions opt
         }
         else
         {
-          throw new cce.UnreachableException();
+          throw new Cce.UnreachableException();
         }
       }
       return wlps[impl.Blocks[0]].Select(assertCmd => Forall(impl.LocVars.Union(impl.OutParams), assertCmd)).ToList();
@@ -442,7 +442,7 @@ private List<AssertCmd> HoistAsserts(List<Cmd> cmds, List<AssertCmd> postconditi
         }
         else
         {
-          throw new cce.UnreachableException();
+          throw new Cce.UnreachableException();
         }
       }
       cmds.RemoveAll(cmd => cmd is AssertCmd);

Source/Concurrency/CivlUtil.cs

@@ -36,7 +36,7 @@ public void Compute()
         }
         else
         {
-          throw new cce.UnreachableException();
+          throw new Cce.UnreachableException();
         }
       }
     }
@@ -108,7 +108,7 @@ private HashSet<Variable> Propagate(Cmd cmd, HashSet<Variable> liveVars)
         liveVars.ExceptWith(stateCmd.Locals);
         return liveVars;
       }
-      throw new cce.UnreachableException();
+      throw new Cce.UnreachableException();
     }
   }
 

Source/Core/AST/Absy.cs

@@ -85,7 +85,7 @@ public virtual Absy Clone()
     {
       Contract.Ensures(Contract.Result<Absy>() != null);
       Absy /*!*/
-        result = cce.NonNull((Absy /*!*/) this.MemberwiseClone());
+        result = Cce.NonNull((Absy /*!*/) this.MemberwiseClone());
       result.UniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); // BUGBUG??
 
       if (InternalNumberedMetadata != null)
@@ -697,7 +697,7 @@ public NamedDeclaration(IToken tok, string name)
     [Pure]
     public override string ToString()
     {
-      return cce.NonNull(Name);
+      return Cce.NonNull(Name);
     }
   }
 
@@ -1061,7 +1061,7 @@ public override void Typecheck(TypecheckingContext tc)
 
     public static void ResolveTypeSynonyms(List<TypeSynonymDecl /*!*/> /*!*/ synonymDecls, ResolutionContext /*!*/ rc)
     {
-      Contract.Requires(cce.NonNullElements(synonymDecls));
+      Contract.Requires(Cce.NonNullElements(synonymDecls));
       Contract.Requires(rc != null);
       // then discover all dependencies between type synonyms
       IDictionary<TypeSynonymDecl /*!*/, List<TypeSynonymDecl /*!*/> /*!*/> /*!*/
@@ -1129,7 +1129,7 @@ private static void FindDependencies(Type /*!*/ type, List<TypeSynonymDecl /*!*/
       ResolutionContext /*!*/ rc)
     {
       Contract.Requires(type != null);
-      Contract.Requires(cce.NonNullElements(deps));
+      Contract.Requires(Cce.NonNullElements(deps));
       Contract.Requires(rc != null);
       if (type.IsVariable || type.IsBasic)
       {
@@ -1331,7 +1331,7 @@ public int Compare(object a, object b)
         throw new ArgumentException("VariableComparer works only on objects of type Variable");
       }
 
-      return cce.NonNull(A.Name).CompareTo(B.Name);
+      return Cce.NonNull(A.Name).CompareTo(B.Name);
     }
   }
 
@@ -1674,12 +1674,12 @@ public DeclWithFormals(IToken tok, string name, List<TypeVariable> typeParams,
     }
 
     protected DeclWithFormals(DeclWithFormals that)
-      : base(that.tok, cce.NonNull(that.Name))
+      : base(that.tok, Cce.NonNull(that.Name))
     {
       Contract.Requires(that != null);
       this.TypeParameters = that.TypeParameters;
-      this.inParams = cce.NonNull(that.InParams);
-      this.outParams = cce.NonNull(that.OutParams);
+      this.inParams = Cce.NonNull(that.InParams);
+      this.outParams = Cce.NonNull(that.OutParams);
     }
 
     public byte[] MD5Checksum_;
@@ -1871,7 +1871,7 @@ protected void EmitSignature(TokenTextWriter stream, bool shortRet)
       {
         Contract.Assert(OutParams.Count == 1);
         stream.Write(" : ");
-        cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
+        Cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
       }
       else if (OutParams.Count > 0)
       {
@@ -2172,11 +2172,11 @@ public override void Typecheck(TypecheckingContext tc)
       {
         Contract.Assert(DefinitionBody == null);
         Body.Typecheck(tc);
-        if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
+        if (!Cce.NonNull(Body.Type).Unify(Cce.NonNull(OutParams[0]).TypedIdent.Type))
         {
           tc.Error(Body,
             "function body with invalid type: {0} (expected: {1})",
-            Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
+            Body.Type, Cce.NonNull(OutParams[0]).TypedIdent.Type);
         }
       }
       else if (DefinitionBody != null)
@@ -2185,11 +2185,11 @@ public override void Typecheck(TypecheckingContext tc)
 
         // We are matching the type of the function body with output param, and not the type
         // of DefinitionBody, which is always going to be bool (since it is of the form func_call == func_body)
-        if (!cce.NonNull(DefinitionBody.Args[1].Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
+        if (!Cce.NonNull(DefinitionBody.Args[1].Type).Unify(Cce.NonNull(OutParams[0]).TypedIdent.Type))
         {
           tc.Error(DefinitionBody.Args[1],
             "function body with invalid type: {0} (expected: {1})",
-            DefinitionBody.Args[1].Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
+            DefinitionBody.Args[1].Type, Cce.NonNull(OutParams[0]).TypedIdent.Type);
         }
       }
     }
@@ -3630,7 +3630,7 @@ public static class Emitter
     public static void Emit(this List<Declaration /*!*/> /*!*/ decls, TokenTextWriter stream)
     {
       Contract.Requires(stream != null);
-      Contract.Requires(cce.NonNullElements(decls));
+      Contract.Requires(Cce.NonNullElements(decls));
       bool first = true;
       foreach (Declaration d in decls)
       {
@@ -3978,7 +3978,7 @@ public static RE Transform(Block b)
         Contract.Assume(g.LabelTargets != null);
         if (g.LabelTargets.Count == 1)
         {
-          return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.LabelTargets[0])));
+          return new Sequential(new AtomicRE(b), Transform(Cce.NonNull(g.LabelTargets[0])));
         }
         else
         {
@@ -3997,7 +3997,7 @@ public static RE Transform(Block b)
       else
       {
         Contract.Assume(false);
-        throw new cce.UnreachableException();
+        throw new Cce.UnreachableException();
       }
     }
   }

Source/Core/AST/AbsyQuant.cs

@@ -691,7 +691,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
         //Contract.Requires(node != null);
         Contract.Ensures(Contract.Result<Expr>() != null);
         FunctionCall fn = node.Fun as FunctionCall;
-        if (fn != null && cce.NonNull(fn.Func).NeverTrigger)
+        if (fn != null && Cce.NonNull(fn.Func).NeverTrigger)
         {
           parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> {node}, parent.Triggers);
         }