Value Analysis Menu Dependency Analysis

Effects Analysis

Click to view full screenshot

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.