Expand description

A fixpoint algorithm analyzing all memory accesses in a program.

The goal of the pointer inference analysis is to keep track of all memory objects and pointers that the program knows about at specific program points during execution. It is a combination of a points-to-analysis and a value-set-analysis. The results of the pointer inference analysis are made available to other analyses, which can use them to look up points-to and value set information.

If the Memory check is enabled, then the analysis also reports some possible memory management errors, like Null pointer dereferences, to the user.

The Memory Check

If the Memory check is enabled, the pointer inference reports instances of CWE-476 (NULL Pointer Dereference) that were detected during the analysis.

The analysis operates on a best-effort basis. In cases where we cannot know whether an error is due to an error in the memory management of the program under analysis or due to inexactness of the pointer inference analysis itself, we try to treat it as the more likely (but not necessarily true) case of the two.

See the Config struct for configurable analysis parameters.

Modules

  • This module contains the definition of the abstract memory object type.

Structs

  • Configurable parameters for the analysis.
  • A wrapper struct for the pointer inference computation object. Also contains different analysis results computed through the fixpoint computation including generated log messages.
  • Contains all information known about the state of a program at a specific point of time.

Statics

  • The name and version number of the “Memory” CWE check.

Functions

  • The entry point for the memory analysis check. Does not actually compute anything but just extracts the results of the already computed pointer inference analysis.
  • Compute the pointer inference analysis and return its results.

Type Aliases

  • The abstract domain type for representing register values.
  • The abstract domain to use for absolute values.