From 6450474dd2a0a2296136ea50df9aa6fe59d0b546 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 13 Nov 2024 17:31:30 +0100
Subject: [PATCH] Provide more flexibility in configuring which return
 statements get separate VCs with isolate_assertions (#979)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### Changes
Enable isolate_assertions to include explicit return statement in Daf…ny
programs
---
 Source/Core/Generic/TokenWrapper.cs                         | 2 ++
 Source/Core/Token.cs                                        | 6 ++++++
 Source/Directory.Build.props                                | 2 +-
 .../VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs   | 2 +-
 4 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/Source/Core/Generic/TokenWrapper.cs b/Source/Core/Generic/TokenWrapper.cs
index d7ea8427d..004fb9f80 100644
--- 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
index 27a0dd156..09e908dee 100644
--- 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
index 7ba4204a9..0fbe10344 100644
--- 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
index b8d8af84a..f41c8973d 100644
--- 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;