diff options
| author |  akashlal <unknown> | 2010-09-01 11:22:32 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-09-01 11:22:32 +0000 |
| commit | ca50aef90076b154b2748d1bf5a8f046452a2aa3 (patch) | |
| tree | 22eba21a2446cc26f8352a6491605a4cb166d409 /Source/VCGeneration/VC.cs | |
| parent | 3c12823d41d9330e92940b728d92b0177e24d11c (diff) | |
Minor fix to my previous commit
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;
}
|