The value analysis plug-in computes sets of possible values for
every variable at each point of the program. When providing such
results, Frama-C guarantees that the variable does not take at that
point any value other than those listed.
When the execution reaches this point inside the loop, the
variable S always contains either 0, 1, 3, or 6.