summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-09-19 20:02:00 -0700
committerGravatar qadeer <unknown>2014-09-19 20:02:00 -0700
commit19a2ca90bdee10b53766fdec679a2cde5b3c3c71 (patch)
treeb1d0b2d6beeb09118bb14c9f57a9297a914c9dd1
parentf8de3b4b9b3acbda2b82522816f1c265954ef5be (diff)
a small fix to prefix calculation
-rw-r--r--Source/Core/Inline.cs30
1 files changed, 17 insertions, 13 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index d6707f1f..4738d855 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -91,38 +91,42 @@ namespace Microsoft.Boogie {
this.prefix = null;
}
- // This method updates inliner.prefix so that prepending it to any string is guaranteed
- // not to create a conflict with any of the in/out/local variables of impl
+ // This method calculates a prefix (storing it in the prefix field) so that prepending it to any string
+ // is guaranteed not to create a conflict with the names of variables and blocks in scope inside impl.
protected void ComputePrefix(Program program, Implementation impl)
{
this.prefix = "inline$";
foreach (var v in impl.InParams)
{
- DistinguishPrefix(v);
+ DistinguishPrefix(v.Name);
}
foreach (var v in impl.OutParams)
{
- DistinguishPrefix(v);
+ DistinguishPrefix(v.Name);
}
foreach (var v in impl.LocVars)
{
- DistinguishPrefix(v);
+ DistinguishPrefix(v.Name);
}
foreach (var v in program.GlobalVariables())
{
- DistinguishPrefix(v);
+ DistinguishPrefix(v.Name);
+ }
+ foreach (Block b in impl.Blocks)
+ {
+ DistinguishPrefix(b.Label);
}
}
- private void DistinguishPrefix(Variable v)
+ private void DistinguishPrefix(string s)
{
- if (!v.Name.StartsWith(prefix)) return;
- for (int i = prefix.Length; i < v.Name.Length; i++)
+ if (!s.StartsWith(prefix)) return;
+ for (int i = prefix.Length; i < s.Length; i++)
{
prefix = prefix + "$";
- if (v.Name[i] != '$') break;
+ if (s[i] != '$') break;
}
- if (prefix == v.Name)
+ if (prefix == s)
{
prefix = prefix + "$";
}
@@ -274,7 +278,7 @@ namespace Microsoft.Boogie {
// increment the counter for the procedure to be used in constructing the locals and formals
NextInlinedProcLabel(impl.Proc.Name);
- BeginInline(newLocalVars, newModifies, impl);
+ BeginInline(impl);
List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel);
Contract.Assert(cce.NonNullElements(inlinedBlocks));
@@ -421,7 +425,7 @@ namespace Microsoft.Boogie {
return newBlocks;
}
- protected void BeginInline(List<Variable> newLocalVars, List<IdentifierExpr> newModifies, Implementation impl) {
+ protected void BeginInline(Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
Contract.Requires(newModifies != null);