fixed crash in resolve and typecheck

boogie-org · Jun 24, 2024 · 3bb2588 · 3bb2588
1 parent 6d3a6c3
commit 3bb2588
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -129,6 +129,7 @@ public static int ResolveAndTypecheck(CoreOptions options, Absy absy)
       }
 
       var tc = new TypecheckingContext(null, options);
+      tc.CheckModifies = false; // to prevent access to tc.Proc which is null
       absy.Typecheck(tc);
       return tc.ErrorCount;
     }
@@ -144,6 +145,7 @@ 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/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs
@@ -651,7 +651,7 @@ private Expr GetExitCondition(Action action)
       return exitCondition == null ? Expr.False : Substituter.Apply(subst, exitCondition);
     }
 
-    protected List<Declaration> GenerateExitPropertyAllPendingAsyncsNotInElimChecker(Action action)
+    protected List<Declaration> GenerateAllPendingAsyncsNotInElimChecker(Action action)
     {
       var eliminatedActionDecls = EliminatedActionDecls.ToHashSet();
       var elimExprs = new List<Expr>();
@@ -675,12 +675,12 @@ protected List<Declaration> GenerateExitPropertyAllPendingAsyncsNotInElimChecker
         GetCheck(action.tok, Expr.And(elimExprs), "Exit condition is true and there is a pending async to an eliminated action."),
       };
 
-      // CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
-      return GetCheckerTuple($"{rule}_ExitProperty_AllPendingAsyncsNotInElim_{action.Name}", new List<Requires>(),
+      CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
+      return GetCheckerTuple($"{rule}_AllPendingAsyncsNotInElim_{action.Name}", new List<Requires>(),
         action.Impl.InParams, action.Impl.OutParams, new List<Variable>(),  cmds);
     }
 
-    protected List<Declaration> GenerateExitPropertyAllPendingAsyncsInElimChecker(Action action)
+    protected List<Declaration> GenerateAllPendingAsyncsInElimChecker(Action action)
     {
       var eliminatedActionDecls = EliminatedActionDecls.ToHashSet();
       var elimExprs = new List<Expr>();
@@ -704,8 +704,8 @@ protected List<Declaration> GenerateExitPropertyAllPendingAsyncsInElimChecker(Ac
         GetCheck(action.tok, Expr.And(notElimExprs), "Exit condition is false and there is a pending async to an action not in eliminated actions."),
       };
 
-      //CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
-      return GetCheckerTuple($"{rule}_ExitProperty_AllPendingAsyncsInElim_{action.Name}", new List<Requires>(),
+      CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
+      return GetCheckerTuple($"{rule}_AllPendingAsyncsInElim_{action.Name}", new List<Requires>(),
         action.Impl.InParams, action.Impl.OutParams, new List<Variable>(),  cmds);
     }
 
@@ -893,8 +893,8 @@ protected override List<Declaration> GenerateCheckers()
         decls.AddRange(GenerateSideConditionChecker(targetAction));
         foreach (var elim in eliminatedActions)
         {
-          decls.AddRange(GenerateExitPropertyAllPendingAsyncsInElimChecker(elim));
-          decls.AddRange(GenerateExitPropertyAllPendingAsyncsNotInElimChecker(elim));
+          decls.AddRange(GenerateAllPendingAsyncsInElimChecker(elim));
+          decls.AddRange(GenerateAllPendingAsyncsNotInElimChecker(elim));
           if (elim == targetAction)
           {
             continue;