2 \defgroup pointer-analysis pointer-analysis
4 # Folder pointer-analysis
6 \author Martin Brain, Chris Smowton
8 To perform symbolic execution on programs with dereferencing of
9 arbitrary pointers, some alias analysis is needed. `pointer-analysis`
10 contains the three levels of analysis; flow and context insensitive,
11 context sensitive and flow and context sensitive. The code needed is
12 subtle and sophisticated and thus there may be bugs.
14 \section pointer-analysis-utilities Utilities:
16 \subsection pointer-analysis-object-numbering Object / expression numbering (object_numberingt)
18 Object numbering assigns numbers to expressions, allowing other pointer-analysis
19 classes to use small, cheap to compare, cheap to sort numbers in place of
20 \ref exprt instances. Numbering also saves memory, as two identical exprt
21 objects will be assigned the same number, eliminating redundant storage of the
24 Alternative approaches to the same problem include \ref irept sharing (but this
25 only shares when a copy is taken; two identical irepts arrived at by different
26 routes will not be shared) and \ref merge_irept (which does merge identical
27 ireps, but is still more expensive to compare than numbers).
29 Object numbering is used by \ref value_sett and cousins (such as
30 \ref value_set_fit) in an effort to reduce the memory dedicated to value-set
33 \subsection pointer-analysis-pointer-offset-sum Pointer-offset sum (pointer_offset_sum)
37 \subsection pointer-analysis-rewrite-index Rewrite index (x[i] -> *(x+i)) (rewrite_index)
41 \section pointer-analysis-analysis Value-set Analysis:
45 \subsection pointer-analysis-variants Variants:
47 \subsubsection pointer-analysis-flow-insensitive Flow-insensitive
51 \subsubsection pointer-analysis-flow-insensitive-with-vr Flow-insensitive with 'vr' (value reduction?)
55 \subsubsection pointer-analysis-flow-insensitive-with-vr-ns Flow-insensitive with 'vr' and 'ns' (value reduction, ???)
59 \section pointer-analysis-transformations Transformations:
61 \subsection pointer-analysis-add-failed-symbols
65 \subsection pointer-analysis-dereference-removal Dereference removal (*x -> x == &o1 ? o1 : ...) -- dereferencet, dereference_callbackt, value_set_dereferencet, goto_program_dereferencet, etc