Open
Description
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:
