add implementation with side effect
shows that frama-c can detect unintended side effects
provide an example with fine tuned assigns clause