Lexical_Loops.h incorrectly advising of an additional loop not in lexical form.

[malkawimahdi]

CBMC version: 5.77 Operating system: Mac OS Ventura 13.2.1 (Arm M1) Exact command line resulting in the issue:

goto-instrument --show-lexical-loops main.goto

What behaviour did you expect: Lexical_Loops.h should not advise of an additional loop not in lexical form. What happened instead: Lexical_Loops.h advised that an additional loop is present, not in lexical form.

A single cycle is present; however, Lexical_Loops.h believes that an additional cycle exists that is not in lexical loop form.

Lexical_Loop.h and Natural_Loops.h correctly detect the single cycle.

// Example generated by Mahdi Malkawi based on:
// Flow Graph Anomalies: What's in a Loop? by Michael Wolfe
// https://scholararchive.ohsu.edu/downloads/9z903022q?locale=en
// Control Flow Graph 5b (G5b:) page 5

int main(int argc, char **argv)
{
    int array[] = {1, 2};
    int length = sizeof(array) / sizeof(array[0]);

    int counter = 0;
    int sum = 0;

l1:

    while (counter < length)
    {
        sum += array[counter];
        ++counter;

        if (sum == 15)
        {
            goto l1;
        }
        else
        {
            break;
        }
    }

    return 0;
}

The output of goto-instrument --show-lexical-loops main.goto :

8 is head of { 8, 9, 10, 11, 12 (backedge) }
Note not all loops are in lexical form

Graphviz of code outlined above using the commands above:

[feliperodri]

cc. @remi-delmas-3000

[feliperodri]

@esteffin are there any soundness implications from this issue?