first commit

boogie-org · Nov 17, 2024 · 1b9a093 · 1b9a093
1 parent 6b8fbed
commit 1b9a093
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 6 deletions.
diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -133,7 +133,6 @@ public static int ResolveAndTypecheck(CoreOptions options, Absy absy, Resolution
       }
 
       var tc = new TypecheckingContext(null, options);
-      tc.CheckModifies = false; // to prevent access to tc.Proc which is null
       absy.Typecheck(tc);
       return tc.ErrorCount;
     }

diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
@@ -530,10 +530,7 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
       return;
     }
     var tc = new TypecheckingContext(null, options);
-    var oldCheckModifies = tc.CheckModifies;
-    tc.CheckModifies = false;
     absys.ForEach(absy => absy.Typecheck(tc));
-    tc.CheckModifies = oldCheckModifies;
   }
 
   private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
@@ -751,13 +751,12 @@ public class TypecheckingContext : CheckingContext
     public LayerRange ExpectedLayerRange;
     public bool GlobalAccessOnlyInOld;
     public int InsideOld;
-    public bool CheckModifies;
+    public bool CheckModifies => Proc != null && (Proc.IsPure || (!Options?.DoModSetAnalysis ?? true));
 
     public TypecheckingContext(IErrorSink errorSink, CoreOptions options)
       : base(errorSink)
     {
       this.Options = options;
-      this.CheckModifies = !options?.DoModSetAnalysis ?? true;
     }
 
     public bool InFrame(Variable v)