diff options
| author |  qadeer <unknown> | 2014-09-30 12:54:29 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-09-30 12:54:29 -0700 |
| commit | 52f5083f45e3ca26baf9fdca434afa5870b006e9 (patch) | |
| tree | 833b6e7d42c867e17406fc0c0579234b4b13fae8 /Source/VCGeneration/VC.cs | |
| parent | 3bff2d35122109b624f233234d657b1dc72e55c3 (diff) | |
fixed StackOverflow in TraceCounterexample;
converted tail recursion into a loop
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 77 |
1 files changed, 41 insertions, 36 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index d7320ef1..6a039923 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2904,44 +2904,49 @@ namespace VC { ProverContext/*!*/ context,
Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)
{
- Contract.Requires(b != null);
- Contract.Requires(traceNodes != null);
- Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
- Contract.Requires(context != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
- // After translation, all potential errors come from asserts.
- List<Cmd> cmds = b.Cmds;
- Contract.Assert(cmds != null);
- TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Count; i++)
- {
- Cmd cmd = cce.NonNull( cmds[i]);
-
- // Skip if 'cmd' not contained in the trace or not an assert
- if (cmd is AssertCmd && traceNodes.Contains(cmd))
- {
- Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context);
- Contract.Assert(newCounterexample != null);
- newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
- return newCounterexample;
- }
- }
-
- GotoCmd gotoCmd = transferCmd as GotoCmd;
- if (gotoCmd != null)
- {
- foreach (Block bb in cce.NonNull(gotoCmd.labelTargets))
+ Contract.Requires(b != null);
+ Contract.Requires(traceNodes != null);
+ Contract.Requires(trace != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
+ Contract.Requires(context != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
+ // After translation, all potential errors come from asserts.
+
+ while (true)
{
- Contract.Assert(bb != null);
- if (traceNodes.Contains(bb)){
- trace.Add(bb);
- return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, context, calleeCounterexamples);
- }
- }
- }
+ List<Cmd> cmds = b.Cmds;
+ Contract.Assert(cmds != null);
+ TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ Cmd cmd = cce.NonNull(cmds[i]);
- return null;
+ // Skip if 'cmd' not contained in the trace or not an assert
+ if (cmd is AssertCmd && traceNodes.Contains(cmd))
+ {
+ Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context);
+ Contract.Assert(newCounterexample != null);
+ newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
+ return newCounterexample;
+ }
+ }
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd == null) return null;
+ Block foundBlock = null;
+ foreach (Block bb in cce.NonNull(gotoCmd.labelTargets))
+ {
+ Contract.Assert(bb != null);
+ if (traceNodes.Contains(bb))
+ {
+ foundBlock = bb;
+ break;
+ }
+ }
+ if (foundBlock == null) return null;
+ trace.Add(foundBlock);
+ b = foundBlock;
+ }
}
public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, List<Block> trace, Model errModel, ModelViewInfo mvInfo, ProverContext context)
|