diff options
| author |  qadeer <unknown> | 2014-09-17 22:43:09 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-09-17 22:43:09 -0700 |
| commit | 3b4b2d1ee8b260b450274ee0ad86d0d2d6743210 (patch) | |
| tree | 07a2051a273190d47fe3c0eca985eaf512b86df7 /Source/Core | |
| parent | 2151f863ce418b3deb50c9a8d955f4b3b72cead6 (diff) | |
fixed a bug in inlining
changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Inline.cs | 52 |
1 files changed, 50 insertions, 2 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 9af18158..47582868 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -35,6 +35,8 @@ namespace Microsoft.Boogie { protected List<IdentifierExpr>/*!*/ newModifies;
+ protected string prefix;
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(program != null);
@@ -72,7 +74,7 @@ namespace Microsoft.Boogie { currentId = 0;
inlinedProcLblMap.Add(procName, currentId);
}
- return "inline$" + procName + "$" + currentId;
+ return prefix + procName + "$" + currentId;
}
protected string GetProcVarName(string procName, string formalName) {
@@ -93,12 +95,58 @@ namespace Microsoft.Boogie { this.inlineCallback = cb;
this.newLocalVars = new List<Variable>();
this.newModifies = new List<IdentifierExpr>();
+ this.prefix = "inline$";
+ }
+
+ protected static void ComputeInlinerPrefix(Implementation impl, Inliner inliner)
+ {
+ foreach (var v in impl.InParams)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
+ foreach (var v in impl.OutParams)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
+ foreach (var v in impl.LocVars)
+ {
+ if (!v.Name.StartsWith(inliner.prefix)) continue;
+ for (int i = inliner.prefix.Length; i < v.Name.Length; i++)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ if (v.Name[i] != '$') break;
+ }
+ if (inliner.prefix == v.Name)
+ {
+ inliner.prefix = inliner.prefix + "$";
+ }
+ }
}
protected static void ProcessImplementation(Implementation impl, Inliner inliner) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
+ ComputeInlinerPrefix(impl, inliner);
+
inliner.newLocalVars.AddRange(impl.LocVars);
inliner.newModifies.AddRange(impl.Proc.Modifies);
@@ -466,7 +514,7 @@ namespace Microsoft.Boogie { }
private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {
- if (QKeyValue.FindBoolAttribute(ens.Attributes, "assume")) {
+ if (QKeyValue.FindBoolAttribute(ens.Attributes, "HoudiniAssume")) {
return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
} else if (ens.Free) {
return new AssumeCmd(ens.tok, Expr.True);
|