diff options
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 348c2ca9..7ec493f4 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -3770,20 +3770,39 @@ namespace VC { for (int pos = 0; pos < block.Cmds.Length; pos++)
{
Cmd cmd = block.Cmds[pos];
+ string procCalled = null;
if (cmd is CallCmd)
{
var cc = (CallCmd)cmd;
if (inlinedProcs.ContainsKey(cc.Proc.Name))
{
- if (i == 1)
+ procCalled = cc.Proc.Name;
+ }
+ }
+
+ if (cmd is AssumeCmd)
+ {
+ var expr = (cmd as AssumeCmd).Expr as NAryExpr;
+ if (expr != null)
+ {
+ if (inlinedProcs.ContainsKey(expr.Fun.FunctionName))
{
- Debug.Assert(cc.Proc.Name == callee);
- return pos;
+ procCalled = expr.Fun.FunctionName;
}
- i--;
}
}
+
+ if (procCalled != null)
+ {
+ if (i == 1)
+ {
+ Debug.Assert(procCalled == callee);
+ return pos;
+ }
+ i--;
+ }
}
+
Debug.Assert(false, "Didn't find the i^th call cmd");
return -1;
}
|