diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 18:05:27 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 18:05:27 +0100 |
| commit | afaeb081ffcc1c258db6eb7c34ba0b04c493919a (patch) | |
| tree | d0b07c3e3082f323e17523a3e695dc18ee61062d /Source/VCGeneration/FixedpointVC.cs | |
| parent | 858d43ff93a0cc9bc30ce55906499fb9157124c9 (diff) | |
More refactoring towards replacing PureCollections.Sequence with List
Diffstat (limited to 'Source/VCGeneration/FixedpointVC.cs')
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 78ed8cb5..ac7ee9be 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -253,7 +253,7 @@ namespace Microsoft.Boogie info.type = AnnotationInfo.AnnotationType.LoopInvariant;
annotationInfo.Add(name, info);
// get file and line info from havoc, if there is...
- if (header.Cmds.Length > 0)
+ if (header.Cmds.Count > 0)
{
PredicateCmd bif = header.Cmds[0] as PredicateCmd;
if (bif != null)
@@ -1177,7 +1177,7 @@ namespace Microsoft.Boogie }
CmdSeq cmds = block.Cmds;
- int len = cmds.Length;
+ int len = cmds.Count;
for (int i = len - 1; i >= 0; i--)
{
if (cmds[i] is CallCmd)
@@ -1657,7 +1657,7 @@ namespace Microsoft.Boogie CmdSeq cmds = b.Cmds;
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; i++)
+ for (int i = 0; i < cmds.Count; i++)
{
Cmd cmd = cce.NonNull(cmds[i]);
@@ -1723,7 +1723,7 @@ namespace Microsoft.Boogie {
RPFP.Node callee = root.Outgoing.Children[pos];
orderedStateIds.Add(new StateId(callee.Outgoing, CALL,info));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
new CalleeCounterexampleInfo(
cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds,
implName2StratifiedInliningInfo[calleeName].impl, false)),
|