Module Memory.String_length

String length abstraction.

This abstract domain implements the technique presented in 1. It abstracts C strings by the position of the first `\0` character within the base memory block.

The length is kept in an underlying numeric domain. Therefore, the domain is implemented as a stack domain, to allow sharing the underlying domain with others.

The domain is stateless, because abstraction is performed by rewriting statements/expressions in C into equivalent ones in Universal over the length variable. Not internal state is required.

1 M. Journault, A. Miné, A. Ouadjaout. Modular static analysis of string manipulations in C programs. SAS 2018. LNCS, vol. 11002.