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
goto-instrument --show-natural-loops main.goto
What behaviour did you expect: Lexical_Loops.h and Natural_Loops.h should not include the unreachable instruction within the cycle detected.
What happened instead: Lexical_Loops.h and Natural_Loops.h detected the unreachable instruction from the control flow graph and included the instruction within the cycle for the CFG.
After reviewing generated CFG diagrams using the commands:
goto-cc main.c -o main.goto
goto-instrument --dot main.goto > main.dot
The CFG diagrams were missing chronological nodes. After some investigation with @martin-cs, the nodes were removed from the diagram as they were detected as unreachable. However, Lexical_Loops.h and Natural_Loops.h include the unreachable nodes within detected cycles.
To generate the included results located as attachments:
lexical-loops-results.txt
natural-loops-results.txt, the commands used are:
goto-cc main.c -o main.goto
goto-instrument --show-lexical-loops main.goto
goto-instrument --show-natural-loops main.goto
In both algorithms, unreachable instruction 14 is included within the detected cycles. To generate all the instructions for the given program the command below is used:
goto-instrument --show-goto-functions main.goto > instructions.txt
Which generates this file:
instructions.txt
Below is code that can cause the outlined instance to occur:
// 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 3, (G3:) page 4
int main(int argc, char **argv)
{
int a = 1;
int b = 2;
int error = 0;
l1:
a += 1;
int counter = 10;
l2:
b += 2;
l3:
if (counter <= 10)
{
--counter;
}
else
{
goto l2;
error = 1;
}
l4:
if (error)
{
goto l3;
}
return 0;
}Graphviz of code outlined above using the commands above:
