Generates a predicate characterizing the domain of the l-value.

Generates a collection of predicates for each l-value that is read by the instruction or the branching condition of the statement. Other kinds of statements, like loops, blocks and exceptions are not visited.

More precisely, for set and call instructions: the written l-values from left-hand-side are not visited, but their inner l-values are visited; any l-value from the right-hand-side of the instruction is also visited.

Emitter used for generating domain assertions.

Creates a visitor that can be used to generate new annotations for all visited instructions. The generated assertions are associated with the local emitter. They are all assigned a valid status by Analysis.emitter.

Creates a visitor that can be used to remove all generated annotations from emitter. This will also remove their associated status.