summaryrefslogtreecommitdiff
path: root/Source/Core/Inline.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-09-17 22:52:08 -0700
committerGravatar qadeer <unknown>2014-09-17 22:52:08 -0700
commit1f99baa7cd1bd3e8cdce7dcd854c416291d114a4 (patch)
tree05b0698a2ef74e0c91d852bb4c294edc1259562a /Source/Core/Inline.cs
parent3b4b2d1ee8b260b450274ee0ad86d0d2d6743210 (diff)
added a comment
Diffstat (limited to 'Source/Core/Inline.cs')
-rw-r--r--Source/Core/Inline.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 47582868..00aa5631 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -98,6 +98,8 @@ namespace Microsoft.Boogie {
this.prefix = "inline$";
}
+ // 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
protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)
{
foreach (var v in impl.InParams)