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, consider 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). Thus, during refinement type checking, we give r types ptr(x) and ptr(y) in each branch respectively. However, at the join point, r could point to either x or y so we must find a type that joins the two pointers. We use the result of the analysis to insert a ghost statement at the end of each branch to convert the pointer to a borrow &mut i32{v: ...} and use it as the join.

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.