Analysing and comprehending C programs that use strings
is hard: using standard library functions for manipulating
strings is not enforced and programs often use complex loops
for the same purpose. We introduce the notion of memoryless
loops that capture some of these string loops and present a
counterexample-guided synthesis approach to summarise
memoryless loops using C standard library functions, which
has applications to testing, optimisation and refactoring.

We prove our summarisation is correct for arbitrary input
strings and evaluate it on a database of loops we gathered
from thirteen open-source programs. Our approach can summarise
over two thirds of memoryless loops in less than
five minutes of computation time per loop. We then show
that these summaries can be used to (1) improve symbolic
execution (2) optimise native code, and (3) refactor code.