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 { + /// + /// True if this token was created during parsing + /// + 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 @@ - 3.4.1 + 3.4.2 net6.0 false Boogie 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 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;