diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
index a6400e232..97b66daf7 100644
--- a/Source/Core/AST/AbsyCmd.cs
+++ b/Source/Core/AST/AbsyCmd.cs
@@ -368,10 +368,9 @@ int FreshAnon()
return anon++;
}
- HashSet allLabels = new HashSet();
+ private readonly HashSet allLabels = new();
- Errors /*!*/
- errorHandler;
+ private readonly Errors /*!*/ errorHandler;
[ContractInvariantMethod]
void ObjectInvariant()
@@ -3445,6 +3444,8 @@ public override void Emit(TokenTextWriter stream, int level)
public class ReturnCmd : TransferCmd
{
+ public QKeyValue Attributes { get; set; }
+
public ReturnCmd(IToken /*!*/ tok)
: base(tok)
{
@@ -3476,6 +3477,8 @@ public class GotoCmd : TransferCmd
[Rep] public List LabelNames;
[Rep] public List LabelTargets;
+ public QKeyValue Attributes { get; set; }
+
[ContractInvariantMethod]
void ObjectInvariant()
{
diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs
index c6ac50740..4cb78df21 100644
--- a/Source/Core/AST/Block.cs
+++ b/Source/Core/AST/Block.cs
@@ -128,7 +128,11 @@ public bool IsLive(Variable v)
return liveVarsBefore.Contains(v);
}
- public Block(IToken tok)
+ public static Block ShallowClone(Block block) {
+ return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd);
+ }
+
+ public Block(IToken tok, TransferCmd cmd)
: this(tok, "", new List(), new ReturnCmd(tok))
{
}
diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs
index e35541b6d..f20360987 100644
--- a/Source/Core/AST/CallCmd.cs
+++ b/Source/Core/AST/CallCmd.cs
@@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
Contract.Assert(a != null);
// These probably won't have IDs, but copy if they do.
if (callId is not null) {
- a.CopyIdWithModificationsFrom(tok, req,
+ (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
id => new TrackedCallRequiresAssumed(callId, id));
}
@@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
#endregion
if (callId is not null) {
- assume.CopyIdWithModificationsFrom(tok, e,
+ (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e,
id => new TrackedCallEnsures(callId, id));
}
diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs
index a24485f89..1f9bbf412 100644
--- a/Source/Core/AST/ICarriesAttributes.cs
+++ b/Source/Core/AST/ICarriesAttributes.cs
@@ -51,23 +51,25 @@ public void AddStringAttribute(IToken tok, string name, string parameter)
Attributes = new QKeyValue(tok, name, new List