Revert isolation (#966)

boogie-org · Oct 15, 2024 · 09093a2 · 09093a2
1 parent ff43b61
commit 09093a2
Show file tree

Hide file tree

Showing 106 changed files with 2,577 additions and 3,437 deletions.
diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -307,16 +307,14 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
-    public static readonly IToken /*!*/ ReportedNoToken = new Token();
-
     public static Block Block(string label, List<Cmd> cmds)
     {
-      return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
+      return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
     }
 
     public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
     {
-      return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
+      return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
     }
   }
 

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -1300,7 +1300,7 @@ public override void Resolve(ResolutionContext rc)
 
     public void ResolveWhere(ResolutionContext rc)
     {
-      if (Attributes.FindBoolAttribute("assumption") && this.TypedIdent.WhereExpr != null)
+      if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null)
       {
         rc.Error(tok, "assumption variable may not be declared with a where clause");
       }
@@ -1315,7 +1315,7 @@ public override void Typecheck(TypecheckingContext tc)
     {
       (this as ICarriesAttributes).TypecheckAttributes(tc);
       this.TypedIdent.Typecheck(tc);
-      if (Attributes.FindBoolAttribute("assumption") && !this.TypedIdent.Type.IsBool)
+      if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool)
       {
         tc.Error(tok, "assumption variable must be of type 'bool'");
       }
@@ -2059,7 +2059,7 @@ public override void Emit(TokenTextWriter stream, int level)
 
       stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function ");
       EmitAttributes(stream);
-      if (Body != null && !Attributes.FindBoolAttribute("inline"))
+      if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline"))
       {
         Contract.Assert(DefinitionBody == null);
         // Boogie inlines any function whose .Body field is non-null.  The parser populates the .Body field
@@ -2069,7 +2069,7 @@ public override void Emit(TokenTextWriter stream, int level)
         stream.Write("{:inline} ");
       }
 
-      if (DefinitionBody != null && !Attributes.FindBoolAttribute("define"))
+      if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define"))
       {
         // Boogie defines any function whose .DefinitionBody field is non-null.  The parser populates the .DefinitionBody field
         // if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then
@@ -2350,7 +2350,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume()
     {
-      return Free && Attributes.FindBoolAttribute("always_assume");
+      return Free && QKeyValue.FindBoolAttribute(Attributes, "always_assume");
     }
 
 
@@ -2490,7 +2490,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume ()
     {
-      return Free && this.Attributes.FindBoolAttribute("always_assume");
+      return Free && QKeyValue.FindBoolAttribute(this.Attributes, "always_assume");
     }
 
     public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv)