Skip to content

Latest commit

 

History

History

pointer-analysis

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
CMakeLists.txt
CMakeLists.txt
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 
add_failed_symbols.cpp
add_failed_symbols.cpp
 
 
add_failed_symbols.h
add_failed_symbols.h
 
 
dereference_callback.h
dereference_callback.h
 
 
goto_program_dereference.cpp
goto_program_dereference.cpp
 
 
goto_program_dereference.h
goto_program_dereference.h
 
 
module_dependencies.txt
module_dependencies.txt
 
 
object_numbering.h
object_numbering.h
 
 
show_value_sets.cpp
show_value_sets.cpp
 
 
show_value_sets.h
show_value_sets.h
 
 
value_set.cpp
value_set.cpp
 
 
value_set.h
value_set.h
 
 
value_set_analysis.cpp
value_set_analysis.cpp
 
 
value_set_analysis.h
value_set_analysis.h
 
 
value_set_analysis_fi.cpp
value_set_analysis_fi.cpp
 
 
value_set_analysis_fi.h
value_set_analysis_fi.h
 
 
value_set_dereference.cpp
value_set_dereference.cpp
 
 
value_set_dereference.h
value_set_dereference.h
 
 
value_set_domain.h
value_set_domain.h
 
 
value_set_domain_fi.cpp
value_set_domain_fi.cpp
 
 
value_set_domain_fi.h
value_set_domain_fi.h
 
 
value_set_fi.cpp
value_set_fi.cpp
 
 
value_set_fi.h
value_set_fi.h
 
 
value_sets.h
value_sets.h
 
 

README.md

\ingroup module_hidden \defgroup pointer-analysis 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.

\section pointer-analysis-utilities Utilities:

\subsection pointer-analysis-object-numbering 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 \ref 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 \ref irept sharing (but this only shares when a copy is taken; two identical ireps arrived at by different routes will not be shared) and \ref merge_irept (which does merge identical ireps, but is still more expensive to compare than numbers).

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

\subsection pointer-analysis-pointer-offset-sum Pointer-offset sum (pointer_offset_sum)

To be documented.

\section pointer-analysis-analysis 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 \ref value_set_analysis_templatet, \ref value_set_domain_templatet and \ref value_sett.

\subsection pointer-analysis-variants Variants:

\subsubsection pointer-analysis-flow-insensitive Flow-insensitive

To be documented.

\section pointer-analysis-transformations Transformations:

\subsection pointer-analysis-add-failed-symbols

This is obsolete.

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

To be documented.