Here&#x27;s an example in a getline implementation: <a href="https:&#x2F;&#x2F;github.com&#x2F;eliteraspberries&#x2F;ttyprompt&#x2F;blob&#x2F;master&#x2F;getline.c#L55" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;eliteraspberries&#x2F;ttyprompt&#x2F;blob&#x2F;master&#x2F;ge...</a><p><pre><code>        &#x2F;*@ loop invariant i;
            loop invariant j &gt;= 0;
            loop assigns j, eol;
         *&#x2F;
        for (j = 0; j &lt; (size_t) i; j++) {
            if (read_buffer[j] == &#x27;\n&#x27;) {
                eol = 1;
                j++;
                break;
            }
        }
</code></pre>
Loop invariants are part of the ACSL specification language, and they can be verified automatically with Frama-C. <a href="http:&#x2F;&#x2F;frama-c.com&#x2F;acsl.html" rel="nofollow">http:&#x2F;&#x2F;frama-c.com&#x2F;acsl.html</a>