[artifact] Misconceptions About Loops in C

<p>NOTE: PLEASE VERIFY INTEGRITY AFTER DOWNLOAD:</p> <p>- SHA-256: eb5dab87eb050ddb23b2041e6e2727ad41a01bb2eeca82dccf1f4517e0114cc8</p> <p>IF HASHES DO NOT MATCH, PLEASE RE-DOWNLOAD AND VERIFY AGAIN.</p> <p>-----------------------------------------------------------------------------------------</p> <p>This artifact collects the examples used in the paper and provides them<br>as a test suite. Each example is a separate program that can be used in a<br>number of ways. The program&rsquo;s text is used in the paper. No results are<br>generated.</p> <p>Each program takes a single input that controls which path through<br>the program is taken and gives a single output that records which branches<br>were taken. This allows them to be used for back-to-back testing with<br>compilers, interpreters, source-to-source translation, or dynamic analysis<br>tools. If the input/output relation changes, then transformation is buggy<br>and unable to handle that kind of loop.</p> <p>They also have assertions that hold true only for valid paths through<br>the program, making them ideal for testing with static analysis tools. If<br>an assertion fails, it indicates a bug in the static analysis tool.<br>To demonstrate how these can be used, we provide a setup to test<br>CBMC.</p>