diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.ssc | 145 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.ssc | 2 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.ssc | 229 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 137 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.ssc | 4 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.ssc | 8 |
6 files changed, 107 insertions, 418 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 35175881..d6d7bbc5 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -279,16 +279,6 @@ namespace Microsoft.Boogie }
/// <summary>
- /// Instrument the "widen" blocks with a statement in the form of "assume J", where J is a loop predicate "variable"
- /// </summary>
- public void InstrumentWithLoopInvariantPredicates()
- {
- foreach (Declaration d in this.TopLevelDeclarations) {
- d.InstrumentWithLoopInvariantPredicates();
- }
- }
-
- /// <summary>
/// Reset the abstract stated computed before
/// </summary>
public void ResetAbstractInterpretationState()
@@ -440,11 +430,6 @@ namespace Microsoft.Boogie public virtual void InstrumentWithInvariants () {}
/// <summary>
- /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks
- /// </summary>
- public virtual void InstrumentWithLoopInvariantPredicates() { /* by default it does nothing */ }
-
- /// <summary>
/// Reset the abstract stated computed before
/// </summary>
public virtual void ResetAbstractInterpretationState() { /* does nothing */ }
@@ -1993,56 +1978,39 @@ namespace Microsoft.Boogie {
if (b.Lattice != null)
{
- CmdSeq newCommands = new CmdSeq();
-
assert b.PreInvariant != null; /* If the pre-abstract state is null, then something is wrong */
-
- Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
- newCommands.Add(cmd);
- newCommands.AddRange(b.Cmds);
-
assert b.PostInvariant != null; /* If the post-state is null, then something is wrong */
- // if(b.Cmds.Length > 0) // If it is not an empty block
- // {
- inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);
- cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
- newCommands.Add(cmd);
- // }
-
- b.Cmds = newCommands;
- }
- }
- }
-
- /// <summary>
- /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks
- /// </summary>
- override public void InstrumentWithLoopInvariantPredicates()
- {
- foreach(Block b in this.Blocks)
- {
- if(b.widenBlock) { // if it is the head of a loop
- CmdSeq newCommands = new CmdSeq();
-
- Block! entryBlock = b;
-
- ICollection<Block!> connectedComponents = this.GetConnectedComponents(b); // Get the connected components from this block
-
- // Duplicate the connected components.
- // Note that as we duplicate all the nodes, in particular we have also to keep track of the *copy* of the entry node.
- // This is the reason why we pass entryBlockByReference
- ICollection<Block!> dupConnectedComponents = duplicate((!) connectedComponents, ref entryBlock);
-
- Expr loopInvariantPredicate = new LoopPredicate(entryBlock, dupConnectedComponents); // Create a new predicate J_{b.Label}
-
- PredicateCmd cmd = new AssumeCmd(Token.NoToken, loopInvariantPredicate);
-
- newCommands.Add(cmd);
- newCommands.AddRange(b.Cmds);
-
- b.Cmds = newCommands;
+ bool instrumentEntry;
+ bool instrumentExit;
+ switch (CommandLineOptions.Clo.InstrumentInfer) {
+ case CommandLineOptions.InstrumentationPlaces.Everywhere:
+ instrumentEntry = true;
+ instrumentExit = true;
+ break;
+ case CommandLineOptions.InstrumentationPlaces.LoopHeaders:
+ instrumentEntry = b.widenBlock;
+ instrumentExit = false;
+ break;
+ default:
+ assert false; // unexpected InstrumentationPlaces value
+ }
+
+ if (instrumentEntry || instrumentExit) {
+ CmdSeq newCommands = new CmdSeq();
+ if (instrumentEntry) {
+ Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ newCommands.Add(cmd);
+ }
+ newCommands.AddRange(b.Cmds);
+ if (instrumentExit) {
+ Expr inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ newCommands.Add(cmd);
+ }
+ b.Cmds = newCommands;
+ }
}
}
}
@@ -2074,8 +2042,6 @@ namespace Microsoft.Boogie }
assert false; // if we are here, it means that the block is not in one of the components. This is an error.
-
- return null; // unreachable code, just to please the compiler
}
/// <summary>
@@ -2164,57 +2130,6 @@ namespace Microsoft.Boogie this.BlockPredecessorsComputed = true;
}
- /// <summary>
- /// Make a deep copy of the set of blocks in the input.
- /// The input must NOT contain two copies of the same block
- /// </summary>
- private ICollection<Block!>! duplicate(ICollection<Block!>! blocks, ref Block! head)
- {
- Dictionary<Block!, Block!> transMap = new Dictionary<Block!, Block!>(); // A map from the old block to a fresh one
-
- foreach(Block! block in blocks) // Create fresh copies for the blocks
- {
- Block! freshBlock = new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); // Construct a copy of the block
- freshBlock.widenBlock = block.widenBlock;
- freshBlock.Predecessors = new BlockSeq();
- transMap.Add(block, freshBlock); // Add a link block -> freshblock
- }
-
- foreach(Block! block in blocks) // Update the references
- {
- Block! freshBlock = transMap[block];
-
- GotoCmd gotoCmd = freshBlock.TransferCmd as GotoCmd;
- if(gotoCmd != null)
- {
- StringSeq! targetNames = new StringSeq();
- BlockSeq! targetBlocks = new BlockSeq();
-
- foreach(Block! next in (!) gotoCmd.labelTargets)
- {
- if(blocks.Contains(next))
- {
- assert transMap[next] != null;
- targetNames.Add(next.Label);
- targetBlocks.Add(transMap[next]);
- }
- }
-
- GotoCmd freshGotoCmd = new GotoCmd(gotoCmd.tok, targetNames, targetBlocks);
- freshBlock.TransferCmd = freshGotoCmd;
- }
- else
- {
- assert freshBlock.TransferCmd is ReturnCmd; // Do nothing as we do not need to update a returnCmd.
- // However, as we want to make the code robust, we check that it is a ReturnCmd
- }
- }
-
- head = transMap[head];
-
- return transMap.Values;
- }
-
public void PruneUnreachableBlocks() {
ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ ();
List<Block!> reachableBlocks = new List<Block!>();
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index 926724cb..41a62515 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -672,7 +672,7 @@ namespace Microsoft.Boogie // Block
public sealed class Block : Absy
{
- public readonly string! Label;
+ public string! Label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
[Rep] [ElementsPeer] public CmdSeq! Cmds;
[Rep] //PM: needed to verify Traverse.Visit
public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index baf12310..eaf4e640 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -836,8 +836,6 @@ namespace Microsoft.Boogie T Visit(FunctionCall! functionCall);
- T Visit(LoopPredicateName! loopPredicateName);
-
T Visit(MapSelect! mapSelect);
T Visit(MapStore! mapStore);
@@ -1572,171 +1570,6 @@ namespace Microsoft.Boogie }
- /// <summary>
- /// A subclass of FunctionCall that stands for a zero-argument function call, used as a loop invariant placeholder
- /// </summary>
- public class LoopPredicateName : FunctionCall
- {
- private Block! block; // The block the predicate refers to
- public Block! Block
- {
- get
- {
- return block;
- }
- }
-
- private string! blockName; // The name of the block
- private ICollection<Block!>! component;
- public ICollection<Block!>! Component
- {
- get
- {
- return this.component;
- }
- }
-
- public string! Name
- {
- get
- {
- return "J_" + this.blockName;
- }
- }
-
- invariant block.Label == blockName; // Note that we ask for object equality of strings...
-
- private Hashtable /* Var -> Incarnations */ preHavocIncarnationMap;
- public Hashtable PreHavocIncarnationMap
- {
- get
- {
- return this.preHavocIncarnationMap;
- }
- }
-
- private Hashtable /* Var -> Incarnations */ postHavocIncarnationMap;
- public Hashtable PostHavocIncarnationMap
- {
- get
- {
- return this.postHavocIncarnationMap;
- }
- }
-
-
- // Those below are the inverse maps of the maps between variables and incarnations
- private Hashtable /* String -> Var */ preHavocIncarnationInverseMap;
- private Hashtable /* String -> Var */ postHavocIncarnationInverseMap;
-
- public Hashtable PreHavocInverseMap
- {
- get
- {
- if(this.preHavocIncarnationInverseMap == null)
- {
- this.preHavocIncarnationInverseMap = new Hashtable();
- assert this.preHavocIncarnationMap != null; // If we get at this point, then something is wrong with the program
- foreach(object! key in (!) (this.preHavocIncarnationMap).Keys)
- {
- object! val = (!) this.preHavocIncarnationMap[key];
- if(!this.preHavocIncarnationInverseMap.ContainsKey(val.ToString()))
- this.preHavocIncarnationInverseMap.Add(val.ToString(), key);
- }
- }
- return this.preHavocIncarnationInverseMap;
- }
- }
-
- public Hashtable PostHavocInverseMap
- {
- get
- {
- if(this.postHavocIncarnationInverseMap == null)
- {
- this.postHavocIncarnationInverseMap = new Hashtable();
- assert this.postHavocIncarnationMap != null; // If it is null, something is wrong before...
- foreach(object! key in (!) (this.postHavocIncarnationMap).Keys)
- {
- object! val = (!) this.postHavocIncarnationMap[key];
- if(!this.postHavocIncarnationInverseMap.ContainsKey(val.ToString()))
- this.postHavocIncarnationInverseMap.Add(val.ToString(), key);
- }
- }
- return this.postHavocIncarnationInverseMap;
- }
- }
-
- /// <summary>
- /// Create a new LoopPredicate
- /// </summary>
- public LoopPredicateName(Block! block, ICollection<Block!>! component)
- : base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool))
- {
- this.block = block;
- this.blockName = block.Label;
- this.component = component;
- // base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool));
- }
-
- public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post)
- {
- assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null;
-
- this.preHavocIncarnationMap = pre;
- this.postHavocIncarnationMap = post;
- }
-
- /// <summary>
- /// Writes down the loop predicate and the incarnations map before and after the havoc statements
- /// </summary>
- public override void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
- string! pre, post;
-
- if(this.postHavocIncarnationMap != null && this.preHavocIncarnationMap != null)
- {
- pre = "pre: [ " + hashtableToString(this.preHavocIncarnationMap) +" ]";
- post = "post: [ " + hashtableToString(this.postHavocIncarnationMap) +" ]";
- }
- else
- {
- pre = post = "[]";
- }
-
- stream.Write("J_" + this.blockName);
- stream.Write("(");
- stream.Write(pre + ", " + post);
- stream.Write(")");
- }
-
- public override Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- return Type.Bool;
- }
-
- public override int ArgumentCount { get { return 0; } }
-
- private string! hashtableToString(Hashtable! map)
- {
- string! outVal = "";
-
- foreach (object! key in map.Keys)
- {
- object val = map[key];
- outVal += key + " -> " + val + ",";
- }
-
- return outVal;
- }
-
- public override T Dispatch<T>(IAppliableVisitor<T>! visitor) {
- return visitor.Visit(this);
- }
-
- }
-
public class NAryExpr : Expr, AI.IFunApp
{
[Additive] [Peer]
@@ -1870,68 +1703,6 @@ namespace Microsoft.Boogie }
}
- /// <summary>
- /// An instance of LoopPredicate stands for a loop invariant predicate
- /// </summary>
- public class LoopPredicate : NAryExpr
- {
- private static ExprSeq! emptyArgs = new ExprSeq(new Expr[0]); // Share the emptylist of arguments among several instances
-
- invariant loopPredicateName == Fun; // loopPredicateName is just a way of subtyping Fun...
- LoopPredicateName! loopPredicateName;
-
- Hashtable /* Var -> Expr */ preHavocIncarnationMap;
- Hashtable /* Var -> Expr */ postHavocIncarnationMap;
-
- private Block! block; // The block the predicate refers to
- private string! BlockName; // Name of the widen block the predicate refers to
- private ICollection<Block!> component; // The component the block belongs to
-
- /// <summary>
- /// Create a predicate (standing for a loop invariant). The parameter are the name of the block and the (strong) connect components the block belongs to
- /// </summary>
- public LoopPredicate(Block! block, ICollection<Block!>! component)
- {
- this.block = block;
- this.BlockName = block.Label;
- this.component = component;
-
- LoopPredicateName! tmp; // to please the compiler we introde a temp variable
- this.loopPredicateName = tmp = new LoopPredicateName(block, component);
- base(Token.NoToken, tmp, emptyArgs); // due to locally computed data
- }
-
- public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post)
- {
- assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null; // The method must be called just once
-
- this.preHavocIncarnationMap = pre;
- this.postHavocIncarnationMap = post;
- this.loopPredicateName.SetPreAndPostHavocIncarnationMaps(pre, post);
- }
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is LoopPredicate)) return false;
-
- LoopPredicate pred = (LoopPredicate) obj;
- return this.BlockName.Equals(pred.BlockName);
- }
-
- [Pure]
- public override int GetHashCode()
- {
- return this.BlockName.GetHashCode();
- }
-
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
- return visitor.VisitLoopPredicate(this);
- }
- }
-
public class MapSelect : IAppliable, AI.IFunctionSymbol {
public readonly int Arity;
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index da8ee0fe..1d16b569 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -75,6 +75,8 @@ namespace Microsoft.Boogie public string! LogPrefix = "";
public bool PrintInstrumented = false;
public bool InstrumentWithAsserts = false;
+ public enum InstrumentationPlaces { LoopHeaders, Everywhere }
+ public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders;
public bool PrintWithUniqueASTIds = false;
private string XmlSinkFilename = null;
[Peer] public XmlSink XmlSink = null;
@@ -604,48 +606,46 @@ namespace Microsoft.Boogie break;
case "-proverWarnings":
- case "/proverWarnings":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/proverWarnings": {
+ int pw = 0;
+ if (ps.GetNumericArgument(ref pw, 3)) {
+ switch (pw) {
+ case 0:
PrintProverWarnings = ProverWarnings.None;
break;
- case "1":
+ case 1:
PrintProverWarnings = ProverWarnings.Stdout;
break;
- case "2":
+ case 2:
PrintProverWarnings = ProverWarnings.Stderr;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-env":
- case "/env":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/env": {
+ int e = 0;
+ if (ps.GetNumericArgument(ref e, 3)) {
+ switch (e) {
+ case 0:
ShowEnv = ShowEnvironment.Never;
break;
- case "1":
+ case 1:
ShowEnv = ShowEnvironment.DuringPrint;
break;
- case "2":
+ case 2:
ShowEnv = ShowEnvironment.Always;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-loopUnroll":
case "/loopUnroll":
@@ -805,64 +805,52 @@ namespace Microsoft.Boogie break;
case "-subsumption":
- case "/subsumption":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/subsumption": {
+ int s = 0;
+ if (ps.GetNumericArgument(ref s, 3)) {
+ switch (s) {
+ case 0:
UseSubsumption = SubsumptionOption.Never;
break;
- case "1":
+ case 1:
UseSubsumption = SubsumptionOption.NotForQuantifiers;
break;
- case "2":
+ case 2:
UseSubsumption = SubsumptionOption.Always;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-liveVariableAnalysis":
- case "/liveVariableAnalysis":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
- LiveVariableAnalysis = false;
- break;
- case "1":
- LiveVariableAnalysis = true;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
+ case "/liveVariableAnalysis": {
+ int lva = 0;
+ if (ps.GetNumericArgument(ref lva, 2)) {
+ LiveVariableAnalysis = lva == 1;
}
break;
+ }
+
+ case "-removeEmptyBlocks":
+ case "/removeEmptyBlocks": {
+ int reb = 0;
+ if (ps.GetNumericArgument(ref reb, 2)) {
+ RemoveEmptyBlocks = reb == 1;
+ }
+ break;
+ }
case "-coalesceBlocks":
- case "/coalesceBlocks":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
- CoalesceBlocks = false;
- break;
- case "1":
- CoalesceBlocks = true;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
+ case "/coalesceBlocks": {
+ int cb = 0;
+ if (ps.GetNumericArgument(ref cb, 2)) {
+ CoalesceBlocks = cb == 1;
}
break;
+ }
case "/DoomDebug":
vcVariety = VCVariety.Doomed;
@@ -983,7 +971,25 @@ namespace Microsoft.Boogie }
}
break;
-
+
+ case "-instrumentInfer":
+ case "/instrumentInfer":
+ if (ps.ConfirmArgumentCount(1)) {
+ switch (args[ps.i])
+ {
+ case "e":
+ InstrumentInfer = InstrumentationPlaces.Everywhere;
+ break;
+ case "h":
+ InstrumentInfer = InstrumentationPlaces.LoopHeaders;
+ break;
+ default:
+ ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
+ break;
+ }
+ }
+ break;
+
case "-vcBrackets":
case "/vcBrackets":
ps.GetNumericArgument(ref BracketIdsInVC, 2);
@@ -1163,7 +1169,6 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||
ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) ||
ps.CheckBooleanFlag("noVerify", ref Verify, false) ||
- ps.CheckBooleanFlag("noRemoveEmptyBlocks", ref RemoveEmptyBlocks, false) ||
ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||
ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) ||
ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||
@@ -1840,7 +1845,6 @@ namespace Microsoft.Boogie p = polyhedra for linear inequalities
s = debug statistics
0..9 = number of iterations before applying a widen (default=0)
- /loopInvOnDemand : Infer loop invariants on demand
/noinfer : turn off the default inference, and overrides the /infer
switch on its left
/checkInfer : instrument inferred invariants as asserts to be checked by
@@ -1849,6 +1853,10 @@ namespace Microsoft.Boogie supported)
/contractInfer : perform procedure contract inference
/logInfer : print debug output during inference
+ /instrumentInfer : h - instrument inferred invariants only at beginning of
+ loop headers (default)
+ e - instrument inferred invariants at beginning and end
+ of every block
/printInstrumented : print Boogie program after it has been
instrumented with invariants
/Houdini[:<flags>] : perform procedure Houdini
@@ -1869,7 +1877,8 @@ namespace Microsoft.Boogie /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis
1 = perform live variable analysis (default)
/noVerify : skip VC generation and invocation of the theorem prover
- /noRemoveEmptyBlocks : do not remove empty blocks during VC generation
+ /removeEmptyBlocks:<c> : 0 - do not remove empty blocks during VC generation
+ 1 - remove empty blocks (default)
/coalesceBlocks:<c> : 0 = do not coalesce blocks
1 = coalesce blocks (default)
/vc:<variety> : n = nested block (default for non-/prover:z3),
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index 506739bf..0686212e 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -197,8 +197,10 @@ namespace Microsoft.Boogie b.Cmds.Add(cmd);
}
b.TransferCmd = succ.TransferCmd;
- if (!b.tok.IsValid && succ.tok.IsValid)
+ if (!b.tok.IsValid && succ.tok.IsValid) {
b.tok = succ.tok;
+ b.Label = succ.Label;
+ }
removedBlocks.Add(succ);
dfsStack.Push(b);
visitedBlocks.Remove(b);
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index c6b50b24..6e50f6db 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -319,14 +319,6 @@ namespace Microsoft.Boogie return node;
}
- /// <summary>
- /// Just invoke VisitNAryExpr
- /// </summary>
- public virtual Expr! VisitLoopPredicate(LoopPredicate! node)
- {
- return this.VisitNAryExpr(node);
- }
-
public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
{
node.Map = (AssignLhs!)this.Visit(node.Map);
|