Interface Overview Menu Effects Analysis

Value Analysis

Click to view full screenshot

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.