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 🔒