For each statement, Frama-C can provide an exhaustive list of
the memory cells that may be modified by this statement during the
execution, even if the statement uses pointers.
Frama-C guarantees that anytime it is executed, the statement
*tmp = S; does not change any memory location other than
the cells of the array T.