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 ireps 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.

Value-set Analysis:

Value-set analysis is a framework for data-flow analyses which involve keeping track of what values different variables can have at different points in the program. The main classes are value_set_analysis_templatet, value_set_domain_templatet and value_sett.

Variants:

Flow-insensitive

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.