Module points_to

This module implements a points-to analysis for mutable references.

We use the result of the analysis to insert ghost statements at the points where pointers (ptr(l)) have to be converted to borrows (&mut T). For example, given the function

fn foo(mut x: i32, mut y: i32, b: bool) {
    let r;
    if b {
        r = &mut x
    } else {
        r = &mut y
    }
}

In the then branch (resp. else) we know r must point to x (resp. y). During refinement checking, we will give r types ptr(x) and ptr(y) in each branch respectively. However, at the join point r could pointn to either x or y. Thus, we use the result of the analysis to insert a ghost statement at the end of each branch to convert the pointers to a borrow &mut T for a type T that needs to be inferred.

Structs

Children 🔒

CollectPointerToBorrows 🔒

Map

Partial mapping from Place to PlaceIndex, where some places also have a ValueIndex.

PlaceIndex 🔒

This index uniquely identifies a place.

PlaceInfo 🔒

This is the information tracked for every PlaceIndex and is stored by Map.

PointsToAnalysis 🔒

This implement a points to analysis for mutable references over a [FlatSet]. The analysis is a may analysis. If you want to know if a reference definitively points to a location you have to combine it with the result of a definitely initialized analysis. See module level documentation for more details.

State 🔒

The dataflow state for the PointsToAnalysis.

ValueIndex 🔒

This index uniquely identifies a tracked place and therefore a slot in State.

Enums

PlaceOrValue 🔒

Used as the result for r-value.

Functions

add_ghost_statements 🔒

debug_with_context 🔒

debug_with_context_rec 🔒

excluded_locals 🔒

Returns all locals with projections that have their reference or address taken.

Type Aliases

Results 🔒