Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/getline.c#L55 https://github.com/eliteraspberries/ttypr

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