cprover
pointer-analysis

Folder pointer-analysis

Author
Martin Brain, Chris Smowton

To perform symbolic execution on programs with dereferencing of arbitrary pointers, some alias analysis is needed. pointer-analysis contains the three levels of analysis; flow and context insensitive, context sensitive and flow and context sensitive. The code needed is subtle and sophisticated and thus there may be bugs.

Utilities:

Object / expression numbering (object_numberingt)

Object numbering assigns numbers to expressions, allowing other pointer-analysis classes to use small, cheap to compare, cheap to sort numbers in place of exprt instances. Numbering also saves memory, as two identical exprt objects will be assigned the same number, eliminating redundant storage of the same data.

Alternative approaches to the same problem include irept sharing (but this only shares when a copy is taken; two identical irepts arrived at by different routes will not be shared) and merge_irept (which does merge identical ireps, but is still more expensive to compare than numbers).

Object numbering is used by value_sett and cousins (such as value_set_fit) in an effort to reduce the memory dedicated to value-set storage.

Pointer-offset sum (pointer_offset_sum)

To be documented.

Rewrite index (x[i] -> *(x+i)) (rewrite_index)

To be documented.

Value-set Analysis:

To be documented.

Variants:

Flow-insensitive

To be documented.

Flow-insensitive with 'vr' (value reduction?)

To be documented.

Flow-insensitive with 'vr' and 'ns' (value reduction, ???)

To be documented.

Transformations:

pointer-analysis-add-failed-symbols

This is obsolete.

Dereference removal (*x -> x == &o1 ? o1 : ...) -- dereferencet, dereference_callbackt, value_set_dereferencet, goto_program_dereferencet, etc

To be documented.