diff options
author | 2010-01-30 19:33:10 +0000 | |
---|---|---|
committer | 2010-01-30 19:33:10 +0000 | |
commit | 08e368784c1ae629d870db6b09edadbef306e1d6 (patch) | |
tree | df1f7832046c0bc9d264eddb4dfe8ed2a958a533 | |
parent | 7fe28b7c23ffd6a458975a117531bdfea6012177 (diff) |
Fixed the implementation of inlining to deal with inlining depth properly.
-rw-r--r-- | Source/Core/Absy.ssc | 3 | ||||
-rw-r--r-- | Source/Core/CommandLineOptions.ssc | 39 | ||||
-rw-r--r-- | Source/Core/Inline.ssc | 132 | ||||
-rw-r--r-- | Test/inline/Answer | 588 | ||||
-rw-r--r-- | Test/inline/runtest.bat | 6 |
5 files changed, 658 insertions, 110 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 00142344..0632d83f 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -1710,7 +1710,8 @@ namespace Microsoft.Boogie return true;
}
- if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.MacroLike) {
+ if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert ||
+ CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) {
Expr? inl = this.FindExprAttribute("inline");
if (inl == null) inl = this.Proc.FindExprAttribute("inline");
if (inl != null && inl is LiteralExpr && ((LiteralExpr)inl).isBigNum && ((LiteralExpr)inl).asBigNum.Signum > 0) {
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index aa07ec41..e3e37ed6 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -217,8 +217,8 @@ namespace Microsoft.Boogie public string StandardLibraryLocation;
// whether procedure inlining is enabled at call sites.
- public enum Inlining { None, MacroLike, Bounded };
- public Inlining ProcedureInlining = Inlining.MacroLike;
+ public enum Inlining { None, Assert, Assume, Spec };
+ public Inlining ProcedureInlining = Inlining.Assume;
public bool PrintInlined = false;
public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };
@@ -894,17 +894,17 @@ namespace Microsoft.Boogie if (ps.ConfirmArgumentCount(1)) {
switch (args[ps.i])
{
- case "m":
- case "macrolike":
- ProcedureInlining = Inlining.MacroLike;
- break;
- case "n":
case "none":
ProcedureInlining = Inlining.None;
break;
- case "b":
- case "bounded":
- ProcedureInlining = Inlining.Bounded;
+ case "assert":
+ ProcedureInlining = Inlining.Assert;
+ break;
+ case "assume":
+ ProcedureInlining = Inlining.Assume;
+ break;
+ case "spec":
+ ProcedureInlining = Inlining.Spec;
break;
default:
ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
@@ -1591,12 +1591,12 @@ namespace Microsoft.Boogie {:inline N}
Inline given procedure (can be also used on implementation).
- With /inline:b, N is the maximal number of inlinings per calling
- procedure (not depth).
- With /inline:m (default), N is ignored, and recursive calls to
- inlined procedure will result in an error.
- With /inline:n the entire attribute is ignored.
- With /inline:m methods with /inline are not verified at all.
+ N should be a non-negative number and represents the inlining depth.
+ With /inline:assume call is replaced with ""assume false"" once inlining depth is reached.
+ With /inline:assert call is replaced with ""assert false"" once inlining depth is reached.
+ With /inline:spec call is left as is once inlining depth is reached.
+ With the above three options, methods with the attribute {:inline N} are not verified.
+ With /inline:none the entire attribute is ignored.
{:verify false}
Skip verification of an implementation.
@@ -1838,9 +1838,10 @@ namespace Microsoft.Boogie i = unsoundly translate bitvectors to integers
/inline:<i> : use inlining strategy <i> for procedures with the :inline
attribute, see /attrHelp for details:
- n = none
- m = macrolike (default)
- b = bounded
+ none
+ assume (default)
+ assert
+ spec
/printInlined : print the implementation after inlining calls to
procedures with the :inline attribute (works with /inline)
/smoke : Soundness Smoke Test: try to stick assert false; in some
diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc index 5c9d18fb..4d633a24 100644 --- a/Source/Core/Inline.ssc +++ b/Source/Core/Inline.ssc @@ -21,12 +21,6 @@ namespace Microsoft.Boogie { private InlineCallback inlineCallback;
private TypecheckingContext! checkingCtx;
- // Maximum number of unrolling per procedure.
- // This is now given as a commnd line option.
- // While typically this number will be given with the :inline attribute in the source code
- // we set this bound in case the programmer does not provide the number along with the :inline attribute.
- public static int MaxUnrollPerProcedure = 3;
-
protected CodeCopier! codeCopier;
protected Dictionary<string!,int>! /* Procedure.Name -> int */ recursiveProcUnrollMap;
@@ -142,21 +136,14 @@ namespace Microsoft.Boogie { // returns true if it is ok to further unroll the procedure
// otherwise, the procedure is not inlined at the call site
- protected bool CheckInline(Implementation! impl) {
+ protected int GetInlineCount(Implementation! impl) {
string! procName = impl.Name;
- int c;
+ int c = -1;
if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
- if(c > 0) {
- if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Bounded) {
- recursiveProcUnrollMap[procName] = c - 1;
- }
- return true;
- }
- recursiveProcUnrollMap[procName] = 0;
- return false;
+ return c;
}
- bool doinline = false;
+ bool findattr = false;
QKeyValue kv = null;
// try proc attributes
@@ -164,64 +151,57 @@ namespace Microsoft.Boogie { kv = impl.Proc.Attributes;
while(kv != null) {
if(kv.Key.Equals("inline")) {
- doinline = true;
+ findattr = true;
break;
}
kv = kv.Next;
}
}
// try impl attributes
- if(!doinline) {
+ if(!findattr) {
kv = impl.Attributes;
while(kv != null) {
if(kv.Key.Equals("inline")) {
- doinline = true;
+ findattr = true;
break;
}
kv = kv.Next;
}
}
- // try impl attributes
- if(doinline) {
+ if (findattr) {
assert(kv != null && kv.Key.Equals("inline"));
- // check the recursion
- if (!recursiveProcUnrollMap.TryGetValue(procName, out c)) {
- c = MaxUnrollPerProcedure;
- if (kv.Params.Count == 1) {
- LiteralExpr lit = kv.Params[0] as LiteralExpr;
- if (lit != null && lit.isBigNum) {
- c = lit.asBigNum.ToIntSafe;
- }
- }
- recursiveProcUnrollMap.Add(procName, c);
+ if (kv.Params.Count == 1) {
+ LiteralExpr lit = kv.Params[0] as LiteralExpr;
+ if (lit != null && lit.isBigNum)
+ c = lit.asBigNum.ToIntSafe;
}
-
- if(c > 0) {
- if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Bounded) {
- recursiveProcUnrollMap[procName] = c - 1;
- }
- return true;
- }
- recursiveProcUnrollMap[procName] = 0;
- return false;
}
- // if not inlined, then record its inline count as 0
- recursiveProcUnrollMap[procName] = 0;
- return false;
+ recursiveProcUnrollMap[procName] = c;
+ return c;
}
+ void CheckRecursion(Implementation! impl, Stack<Procedure!>! callStack) {
+ foreach (Procedure! p in callStack) {
+ if (p == impl.Proc) {
+ string msg = "";
+ foreach (Procedure! p in callStack) {
+ msg = p.Name + " -> " + msg;
+ }
+ msg += p.Name;
+ checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg);
+ }
+ }
+ }
private List<Block!>! DoInlineBlocks(Stack<Procedure!>! callStack, List<Block!>! blocks, Program! program,
VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, ref bool inlinedSomething)
{
List<Block!>! newBlocks = new List<Block!>();
- foreach(Block block in blocks) {
-
+ foreach(Block block in blocks) {
TransferCmd! transferCmd = (!) block.TransferCmd;
-
CmdSeq cmds = block.Cmds;
CmdSeq newCmds = new CmdSeq();
Block newBlock;
@@ -229,54 +209,36 @@ namespace Microsoft.Boogie { int lblCount = 0;
for(int i = 0; i < cmds.Length; ++i) {
- Cmd cmd = cmds[i];
-
+ Cmd cmd = cmds[i];
CallCmd callCmd = cmd as CallCmd;
if(callCmd == null) {
// if not call command, leave it as is
- newCmds.Add(codeCopier.CopyCmd(cmd));
-
+ newCmds.Add(codeCopier.CopyCmd(cmd));
} else {
assert(callCmd.Proc != null);
Procedure proc = null;
Implementation impl = null;
string calleeName = callCmd.Proc.Name;
- bool inline = false;
+ int inline = -1;
// *** now we do not allow constructors to be inlined
- if(! calleeName.Contains("..ctor")) {
+ if (!calleeName.Contains("..ctor")) {
// FIXME why on earth are we searching by name?!
bool implExists = FindProcImpl(program, calleeName, out proc, out impl);
assume(!implExists || (proc != null && impl != null));
- if(implExists) {
- if(CheckInline((!)impl)) {
- inline = true;
- inlinedSomething = true;
- }
+ if (implExists) {
+ inline = GetInlineCount((!)impl);
}
- }
-
- if (impl != null && CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.MacroLike) {
- foreach (Procedure! p in callStack) {
- if (p == impl.Proc) {
- inline = false;
- string msg = "";
- foreach (Procedure! p in callStack) {
- msg = p.Name + " -> " + msg;
- }
- msg += p.Name;
- checkingCtx.Error(impl, "the inlined procedure is recursive, call stack: {0}", msg);
- }
- }
- }
+ }
- assert(!inline || (impl != null));
+ assert(inline == -1 || impl != null);
- if(inline) { // at least one block should exist
+ if (inline > 0) { // at least one block should exist
assume(impl != null && proc != null);
assert(((!)impl.OriginalBlocks).Count > 0);
+ inlinedSomething = true;
// do inline now
int nextlblCount = lblCount + 1;
@@ -296,9 +258,11 @@ namespace Microsoft.Boogie { EndInline();
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
callStack.Push((!)impl.Proc);
inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
callStack.Pop();
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
Block! startBlock = inlinedBlocks[0];
@@ -309,11 +273,21 @@ namespace Microsoft.Boogie { newBlocks.AddRange(inlinedBlocks);
lblCount = nextlblCount;
- newCmds = new CmdSeq();
-
+ newCmds = new CmdSeq();
+ } else if (inline == 0) {
+ inlinedSomething = true;
+ if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
+ // add assert
+ newCmds.Add(new AssertCmd(callCmd.tok, Expr.False));
+ } else if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) {
+ // add assume
+ newCmds.Add(new AssumeCmd(callCmd.tok, Expr.False));
+ } else {
+ // add call
+ newCmds.Add(codeCopier.CopyCmd(callCmd));
+ }
} else {
- // if this call will not be inlined, so leave it as is
- newCmds.Add(codeCopier.CopyCmd(callCmd));
+ newCmds.Add(codeCopier.CopyCmd(callCmd));
}
}
}
diff --git a/Test/inline/Answer b/Test/inline/Answer index c59772cd..d5a12321 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -880,6 +880,586 @@ Execution trace: <console>(98,0): anon3
Boogie program verifier finished with 0 verified, 4 errors
+-------------------- test6.bpl --------------------
+
+procedure {:inline 2} foo();
+ modifies x;
+
+
+
+implementation foo()
+{
+
+ anon0:
+ x := x + 1;
+ call foo();
+ return;
+}
+
+
+
+procedure {:inline 2} foo1();
+ modifies x;
+
+
+
+implementation foo1()
+{
+
+ anon0:
+ x := x + 1;
+ call foo2();
+ return;
+}
+
+
+
+procedure {:inline 2} foo2();
+ modifies x;
+
+
+
+implementation foo2()
+{
+
+ anon0:
+ x := x + 1;
+ call foo3();
+ return;
+}
+
+
+
+procedure {:inline 2} foo3();
+ modifies x;
+
+
+
+implementation foo3()
+{
+
+ anon0:
+ x := x + 1;
+ call foo1();
+ return;
+}
+
+
+
+var x: int;
+
+procedure bar();
+ modifies x;
+
+
+
+implementation bar()
+{
+
+ anon0:
+ call foo();
+ call foo1();
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo();
+ modifies x;
+
+
+implementation foo()
+{
+ var inline$foo$0$x: int;
+ var inline$foo$1$x: int;
+
+ anon0:
+ x := x + 1;
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$x := x;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ x := x + 1;
+ goto inline$foo$1$Entry;
+
+ inline$foo$1$Entry:
+ inline$foo$1$x := x;
+ goto inline$foo$1$anon0;
+
+ inline$foo$1$anon0:
+ x := x + 1;
+ call foo();
+ goto inline$foo$1$Return;
+
+ inline$foo$1$Return:
+ goto inline$foo$0$anon0$1;
+
+ inline$foo$0$anon0$1:
+ goto inline$foo$0$Return;
+
+ inline$foo$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo1();
+ modifies x;
+
+
+implementation foo1()
+{
+ var inline$foo2$0$x: int;
+ var inline$foo3$0$x: int;
+ var inline$foo1$0$x: int;
+ var inline$foo2$1$x: int;
+ var inline$foo3$1$x: int;
+ var inline$foo1$1$x: int;
+
+ anon0:
+ x := x + 1;
+ goto inline$foo2$0$Entry;
+
+ inline$foo2$0$Entry:
+ inline$foo2$0$x := x;
+ goto inline$foo2$0$anon0;
+
+ inline$foo2$0$anon0:
+ x := x + 1;
+ goto inline$foo3$0$Entry;
+
+ inline$foo3$0$Entry:
+ inline$foo3$0$x := x;
+ goto inline$foo3$0$anon0;
+
+ inline$foo3$0$anon0:
+ x := x + 1;
+ goto inline$foo1$0$Entry;
+
+ inline$foo1$0$Entry:
+ inline$foo1$0$x := x;
+ goto inline$foo1$0$anon0;
+
+ inline$foo1$0$anon0:
+ x := x + 1;
+ goto inline$foo2$1$Entry;
+
+ inline$foo2$1$Entry:
+ inline$foo2$1$x := x;
+ goto inline$foo2$1$anon0;
+
+ inline$foo2$1$anon0:
+ x := x + 1;
+ goto inline$foo3$1$Entry;
+
+ inline$foo3$1$Entry:
+ inline$foo3$1$x := x;
+ goto inline$foo3$1$anon0;
+
+ inline$foo3$1$anon0:
+ x := x + 1;
+ goto inline$foo1$1$Entry;
+
+ inline$foo1$1$Entry:
+ inline$foo1$1$x := x;
+ goto inline$foo1$1$anon0;
+
+ inline$foo1$1$anon0:
+ x := x + 1;
+ call foo2();
+ goto inline$foo1$1$Return;
+
+ inline$foo1$1$Return:
+ goto inline$foo3$1$anon0$1;
+
+ inline$foo3$1$anon0$1:
+ goto inline$foo3$1$Return;
+
+ inline$foo3$1$Return:
+ goto inline$foo2$1$anon0$1;
+
+ inline$foo2$1$anon0$1:
+ goto inline$foo2$1$Return;
+
+ inline$foo2$1$Return:
+ goto inline$foo1$0$anon0$1;
+
+ inline$foo1$0$anon0$1:
+ goto inline$foo1$0$Return;
+
+ inline$foo1$0$Return:
+ goto inline$foo3$0$anon0$1;
+
+ inline$foo3$0$anon0$1:
+ goto inline$foo3$0$Return;
+
+ inline$foo3$0$Return:
+ goto inline$foo2$0$anon0$1;
+
+ inline$foo2$0$anon0$1:
+ goto inline$foo2$0$Return;
+
+ inline$foo2$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo2();
+ modifies x;
+
+
+implementation foo2()
+{
+ var inline$foo3$0$x: int;
+ var inline$foo1$0$x: int;
+ var inline$foo2$0$x: int;
+ var inline$foo3$1$x: int;
+ var inline$foo1$1$x: int;
+ var inline$foo2$1$x: int;
+
+ anon0:
+ x := x + 1;
+ goto inline$foo3$0$Entry;
+
+ inline$foo3$0$Entry:
+ inline$foo3$0$x := x;
+ goto inline$foo3$0$anon0;
+
+ inline$foo3$0$anon0:
+ x := x + 1;
+ goto inline$foo1$0$Entry;
+
+ inline$foo1$0$Entry:
+ inline$foo1$0$x := x;
+ goto inline$foo1$0$anon0;
+
+ inline$foo1$0$anon0:
+ x := x + 1;
+ goto inline$foo2$0$Entry;
+
+ inline$foo2$0$Entry:
+ inline$foo2$0$x := x;
+ goto inline$foo2$0$anon0;
+
+ inline$foo2$0$anon0:
+ x := x + 1;
+ goto inline$foo3$1$Entry;
+
+ inline$foo3$1$Entry:
+ inline$foo3$1$x := x;
+ goto inline$foo3$1$anon0;
+
+ inline$foo3$1$anon0:
+ x := x + 1;
+ goto inline$foo1$1$Entry;
+
+ inline$foo1$1$Entry:
+ inline$foo1$1$x := x;
+ goto inline$foo1$1$anon0;
+
+ inline$foo1$1$anon0:
+ x := x + 1;
+ goto inline$foo2$1$Entry;
+
+ inline$foo2$1$Entry:
+ inline$foo2$1$x := x;
+ goto inline$foo2$1$anon0;
+
+ inline$foo2$1$anon0:
+ x := x + 1;
+ call foo3();
+ goto inline$foo2$1$Return;
+
+ inline$foo2$1$Return:
+ goto inline$foo1$1$anon0$1;
+
+ inline$foo1$1$anon0$1:
+ goto inline$foo1$1$Return;
+
+ inline$foo1$1$Return:
+ goto inline$foo3$1$anon0$1;
+
+ inline$foo3$1$anon0$1:
+ goto inline$foo3$1$Return;
+
+ inline$foo3$1$Return:
+ goto inline$foo2$0$anon0$1;
+
+ inline$foo2$0$anon0$1:
+ goto inline$foo2$0$Return;
+
+ inline$foo2$0$Return:
+ goto inline$foo1$0$anon0$1;
+
+ inline$foo1$0$anon0$1:
+ goto inline$foo1$0$Return;
+
+ inline$foo1$0$Return:
+ goto inline$foo3$0$anon0$1;
+
+ inline$foo3$0$anon0$1:
+ goto inline$foo3$0$Return;
+
+ inline$foo3$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+after inlining procedure calls
+procedure {:inline 2} foo3();
+ modifies x;
+
+
+implementation foo3()
+{
+ var inline$foo1$0$x: int;
+ var inline$foo2$0$x: int;
+ var inline$foo3$0$x: int;
+ var inline$foo1$1$x: int;
+ var inline$foo2$1$x: int;
+ var inline$foo3$1$x: int;
+
+ anon0:
+ x := x + 1;
+ goto inline$foo1$0$Entry;
+
+ inline$foo1$0$Entry:
+ inline$foo1$0$x := x;
+ goto inline$foo1$0$anon0;
+
+ inline$foo1$0$anon0:
+ x := x + 1;
+ goto inline$foo2$0$Entry;
+
+ inline$foo2$0$Entry:
+ inline$foo2$0$x := x;
+ goto inline$foo2$0$anon0;
+
+ inline$foo2$0$anon0:
+ x := x + 1;
+ goto inline$foo3$0$Entry;
+
+ inline$foo3$0$Entry:
+ inline$foo3$0$x := x;
+ goto inline$foo3$0$anon0;
+
+ inline$foo3$0$anon0:
+ x := x + 1;
+ goto inline$foo1$1$Entry;
+
+ inline$foo1$1$Entry:
+ inline$foo1$1$x := x;
+ goto inline$foo1$1$anon0;
+
+ inline$foo1$1$anon0:
+ x := x + 1;
+ goto inline$foo2$1$Entry;
+
+ inline$foo2$1$Entry:
+ inline$foo2$1$x := x;
+ goto inline$foo2$1$anon0;
+
+ inline$foo2$1$anon0:
+ x := x + 1;
+ goto inline$foo3$1$Entry;
+
+ inline$foo3$1$Entry:
+ inline$foo3$1$x := x;
+ goto inline$foo3$1$anon0;
+
+ inline$foo3$1$anon0:
+ x := x + 1;
+ call foo1();
+ goto inline$foo3$1$Return;
+
+ inline$foo3$1$Return:
+ goto inline$foo2$1$anon0$1;
+
+ inline$foo2$1$anon0$1:
+ goto inline$foo2$1$Return;
+
+ inline$foo2$1$Return:
+ goto inline$foo1$1$anon0$1;
+
+ inline$foo1$1$anon0$1:
+ goto inline$foo1$1$Return;
+
+ inline$foo1$1$Return:
+ goto inline$foo3$0$anon0$1;
+
+ inline$foo3$0$anon0$1:
+ goto inline$foo3$0$Return;
+
+ inline$foo3$0$Return:
+ goto inline$foo2$0$anon0$1;
+
+ inline$foo2$0$anon0$1:
+ goto inline$foo2$0$Return;
+
+ inline$foo2$0$Return:
+ goto inline$foo1$0$anon0$1;
+
+ inline$foo1$0$anon0$1:
+ goto inline$foo1$0$Return;
+
+ inline$foo1$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ return;
+}
+
+
+after inlining procedure calls
+procedure bar();
+ modifies x;
+
+
+implementation bar()
+{
+ var inline$foo$0$x: int;
+ var inline$foo$1$x: int;
+ var inline$foo1$0$x: int;
+ var inline$foo2$0$x: int;
+ var inline$foo3$0$x: int;
+ var inline$foo1$1$x: int;
+ var inline$foo2$1$x: int;
+ var inline$foo3$1$x: int;
+
+ anon0:
+ goto inline$foo$0$Entry;
+
+ inline$foo$0$Entry:
+ inline$foo$0$x := x;
+ goto inline$foo$0$anon0;
+
+ inline$foo$0$anon0:
+ x := x + 1;
+ goto inline$foo$1$Entry;
+
+ inline$foo$1$Entry:
+ inline$foo$1$x := x;
+ goto inline$foo$1$anon0;
+
+ inline$foo$1$anon0:
+ x := x + 1;
+ call foo();
+ goto inline$foo$1$Return;
+
+ inline$foo$1$Return:
+ goto inline$foo$0$anon0$1;
+
+ inline$foo$0$anon0$1:
+ goto inline$foo$0$Return;
+
+ inline$foo$0$Return:
+ goto anon0$1;
+
+ anon0$1:
+ goto inline$foo1$0$Entry;
+
+ inline$foo1$0$Entry:
+ inline$foo1$0$x := x;
+ goto inline$foo1$0$anon0;
+
+ inline$foo1$0$anon0:
+ x := x + 1;
+ goto inline$foo2$0$Entry;
+
+ inline$foo2$0$Entry:
+ inline$foo2$0$x := x;
+ goto inline$foo2$0$anon0;
+
+ inline$foo2$0$anon0:
+ x := x + 1;
+ goto inline$foo3$0$Entry;
+
+ inline$foo3$0$Entry:
+ inline$foo3$0$x := x;
+ goto inline$foo3$0$anon0;
+
+ inline$foo3$0$anon0:
+ x := x + 1;
+ goto inline$foo1$1$Entry;
+
+ inline$foo1$1$Entry:
+ inline$foo1$1$x := x;
+ goto inline$foo1$1$anon0;
+
+ inline$foo1$1$anon0:
+ x := x + 1;
+ goto inline$foo2$1$Entry;
+
+ inline$foo2$1$Entry:
+ inline$foo2$1$x := x;
+ goto inline$foo2$1$anon0;
+
+ inline$foo2$1$anon0:
+ x := x + 1;
+ goto inline$foo3$1$Entry;
+
+ inline$foo3$1$Entry:
+ inline$foo3$1$x := x;
+ goto inline$foo3$1$anon0;
+
+ inline$foo3$1$anon0:
+ x := x + 1;
+ call foo1();
+ goto inline$foo3$1$Return;
+
+ inline$foo3$1$Return:
+ goto inline$foo2$1$anon0$1;
+
+ inline$foo2$1$anon0$1:
+ goto inline$foo2$1$Return;
+
+ inline$foo2$1$Return:
+ goto inline$foo1$1$anon0$1;
+
+ inline$foo1$1$anon0$1:
+ goto inline$foo1$1$Return;
+
+ inline$foo1$1$Return:
+ goto inline$foo3$0$anon0$1;
+
+ inline$foo3$0$anon0$1:
+ goto inline$foo3$0$Return;
+
+ inline$foo3$0$Return:
+ goto inline$foo2$0$anon0$1;
+
+ inline$foo2$0$anon0$1:
+ goto inline$foo2$0$Return;
+
+ inline$foo2$0$Return:
+ goto inline$foo1$0$anon0$1;
+
+ inline$foo1$0$anon0$1:
+ goto inline$foo1$0$Return;
+
+ inline$foo1$0$Return:
+ goto anon0$2;
+
+ anon0$2:
+ return;
+}
+
+
+
+Boogie program verifier finished with 5 verified, 0 errors
-------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -894,14 +1474,6 @@ Execution trace: test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
--------------------- test6.bpl --------------------
-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
-test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
-test6.bpl(22,22): Error: the inlined procedure is recursive, call stack: foo3 -> foo1 -> foo2 -> foo3
-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
-test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
-test6.bpl(8,22): Error: the inlined procedure is recursive, call stack: foo1 -> foo2 -> foo3 -> foo1
-6 type checking errors detected in test6.bpl
-------------------- expansion.bpl --------------------
expansion.bpl(29,14): Error: invalid type for argument 0 in application of foo1: bool (expected: int)
expansion.bpl(13,16): Error: expansion: {:inline ...} expects either true or false as the argument
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index 209845e6..335c857d 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -8,12 +8,12 @@ for %%f in (test0.bpl) do ( %BGEXE% %* %%f
)
-for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl) do (
+for %%f in (test1.bpl test2.bpl test3.bpl test4.bpl test6.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% %* /inline:b /print:- /env:0 /printInlined /noinfer %%f
+ %BGEXE% %* /inline:spec /print:- /env:0 /printInlined /noinfer %%f
)
-for %%f in (test5.bpl test6.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
+for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
|