Add test and fix bug in RevealedAnalysis

Source/Core/AST/ChangeScope.cs

@@ -24,6 +24,8 @@ public override void Typecheck(TypecheckingContext tc) {
   }
 
   public override void Emit(TokenTextWriter stream, int level) {
+    stream.Write(this, level, Mode == Modes.Push ? "push" : "pop");
+    stream.WriteLine(";");
   }
 
   public override void AddAssignedVariables(List<Variable> vars) {

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.0</Version>
+    <Version>3.2.1</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/VCGeneration/Prune/RevealedAnalysis.cs

@@ -2,6 +2,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.Diagnostics;
 using Microsoft.Boogie;
 
 namespace VCGeneration.Prune;
@@ -27,10 +28,14 @@ public RevealedAnalysis(IReadOnlyList<Cmd> roots,
     RevealedState.AllRevealed);
 
   protected override ImmutableStack<RevealedState> Merge(ImmutableStack<RevealedState> first, ImmutableStack<RevealedState> second) {
-    var firstTop = first.Peek();
-    var secondTop = second.Peek();
-    var mergedTop = MergeStates(firstTop, secondTop);
-    return ImmutableStack.Create(mergedTop);
+    if (first.IsEmpty && second.IsEmpty) {
+      return ImmutableStack<RevealedState>.Empty;
+    }
+    var firstElement = first.Peek();
+    var secondElement = second.Peek();
+    var mergedTop = MergeStates(firstElement, secondElement);
+    var mergedTail = Merge(first.Pop(), second.Pop());
+    return mergedTail.Push(mergedTop);
   }
 
   protected override bool StateEquals(ImmutableStack<RevealedState> first, ImmutableStack<RevealedState> second) {
@@ -77,10 +82,12 @@ static RevealedState GetUpdatedState(HideRevealCmd hideRevealCmd, RevealedState
   }
 
   protected override ImmutableStack<RevealedState> Update(Cmd node, ImmutableStack<RevealedState> state) {
+    if (state.IsEmpty) {
+      throw new Exception("Unbalanced use of push and pop commands");
+    }
+
     if (node is ChangeScope changeScope) {
-      return changeScope.Mode == ChangeScope.Modes.Push 
-        ? state.Push(state.Peek()) 
-        : state.Pop();
+      return changeScope.Mode == ChangeScope.Modes.Push ? state.Push(state.Peek()) : state.Pop();
     }
 
     if (node is HideRevealCmd hideRevealCmd) {

Test/pruning/Reveal.bpl

@@ -40,4 +40,15 @@ procedure Scoping() {
   assert outer(2) == inner(2) + 1;
   pop;
   assert outer(3) == inner(3) + 1; // error
+}
+
+procedure Nesting() {
+  hide *;
+  push;
+  push;
+  if (*) {
+    reveal outer;
+  }
+  pop;
+  pop;
 }

Test/pruning/Reveal.bpl.expect

@@ -3,4 +3,4 @@ Reveal.bpl(29,7): Error: this assertion could not be proved
 Reveal.bpl(31,7): Error: this assertion could not be proved
 Reveal.bpl(42,3): Error: this assertion could not be proved
 
-Boogie program verifier finished with 0 verified, 4 errors
+Boogie program verifier finished with 1 verified, 4 errors