Provide more flexibility in configuring which return statements get s…

…eparate VCs with isolate_assertions (#979) ### Changes Enable isolate_assertions to include explicit return statement in Daf…ny programs
boogie-org · Nov 13, 2024 · 6450474 · 6450474
1 parent 92e40bd
commit 6450474
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 2 deletions.
diff --git a/Source/Core/Generic/TokenWrapper.cs b/Source/Core/Generic/TokenWrapper.cs
@@ -14,6 +14,8 @@ public int CompareTo(IToken? other) {
     return Inner.CompareTo(other);
   }
 
+  public bool IsSourceToken => false;
+
   public int kind {
     get => Inner.kind;
     set => Inner.kind = value;

diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs
@@ -9,6 +9,10 @@ namespace Microsoft.Boogie
   [Immutable]
   public interface IToken : IComparable<IToken>
   {
+    /// <summary>
+    /// True if this token was created during parsing
+    /// </summary>
+    bool IsSourceToken { get; }
     int kind { get; set; } // token kind
     string filename { get; set; } // token file
     int pos { get; set; } // token position in the source text (starting at 0)
@@ -48,6 +52,8 @@ public Token(int linenum, int colnum)
       this._val = "anything so that it is nonnull";
     }
 
+    public bool IsSourceToken => true;
+
     public int kind
     {
       get { return this._kind; }

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.4.1</Version>
+    <Version>3.4.2</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs
@@ -33,7 +33,7 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
 
       var gotoFromReturn = gotoCmd.tok as GotoFromReturn;
       var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate");
-      var isTypeOfAssert = gotoFromReturn != null && gotoFromReturn.Origin.tok is Token;
+      var isTypeOfAssert = gotoFromReturn != null && gotoFromReturn.Origin.tok.IsSourceToken;
       var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute);
       if (!isolate) {
         continue;