Rename class

dafny-lang · Jan 13, 2025 · 579ca74 · 579ca74
1 parent 85346c8
commit 579ca74
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/...ver/FunctionEntanglementChecks_Visitor.cs → ...etectUnsoundFunctionReferences_Visitor.cs b/...ver/FunctionEntanglementChecks_Visitor.cs → ...etectUnsoundFunctionReferences_Visitor.cs
@@ -2,10 +2,10 @@
 
 namespace Microsoft.Dafny;
 
-class FunctionEntanglementChecks_Visitor : ResolverBottomUpVisitor {
+class DetectUnsoundFunctionReferences_Visitor : ResolverBottomUpVisitor {
   private readonly ICallable context;
   public bool DoDecreasesChecks;
-  public FunctionEntanglementChecks_Visitor(ModuleResolver resolver, ICallable context)
+  public DetectUnsoundFunctionReferences_Visitor(ModuleResolver resolver, ICallable context)
     : base(resolver) {
     Contract.Requires(resolver != null);
     Contract.Requires(context != null);

diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -1265,7 +1265,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
       // A function is not allowed to be used naked in its own SCC. Also, a function is not allowed to be used
       // in any way inside a "decreases" clause its its own SCC.
       foreach (var function in ModuleDefinition.AllFunctions(declarations)) {
-        var visitor = new FunctionEntanglementChecks_Visitor(this, function);
+        var visitor = new DetectUnsoundFunctionReferences_Visitor(this, function);
         visitor.Visit(function);
         visitor.DoDecreasesChecks = true;
         visitor.Visit(function.Decreases.Expressions);