[artifact69] Common Misconceptions About Loops in C

This artefact contains the examples used in the paper and presents them as a practical test suite. The paper uses the program text, and no generated results are provided. Each example is a separate program and can be used in several ways. Each program takes a single input which controls the path taken through the program and gives a single output which records which branches were taken. This allows them to be used for back-to-back testing with compilers, interpreters, source-to-source translation or dynamic analysis tools. If the input/output relation changes, then transformation is buggy and unable to handle that kind of loop. Each program also has assertions that are only true for valid paths through the program. These assertions allow the test cases to be used to test static analysis tools. If an assertion fails, it indicates a bug in the static analysis tool. To demonstrate how these can be used, we provide a usable set-up to test the provided examples with cbmc.