•Idea: count a value only if its var was just modified
•Front end outputs modification bit per value
–compared techniques for eliminating duplicates
•Result: eliminates undesired invariants
A variable value
contributes to invariant confidence at a program point if the variable was
assigned to since the last time the program point was executed.
[Tell the concept
here, not just the implementation.]
You can think of
this as a dirty bit.
[No need to avoid
the term “lvalue”.Used to say “at
each assignment, timestamp the lvalue”.]
Actually there is a
bit per lvalue/program point pair.
[Used to say “if
small test suite, eliminates desired invariants”; but don’t raise that red
flag.]
Don’t check just
whether the value is the same, but whether the variable holding that value
was assigned to.
