Trait move_stackless_bytecode::compositional_analysis::CompositionalAnalysis

pub trait CompositionalAnalysis<Summary: AbstractDomain + 'static>: DataflowAnalysis where
    Self::State: AbstractDomain + 'static, {
    fn to_summary(
        &self, 
        state: Self::State, 
        fun_target: &FunctionTarget<'_>
    ) -> Summary;

    fn summarize(
        &self, 
        fun_target: &FunctionTarget<'_>, 
        initial_state: Self::State
    ) -> Summary { ... }
}

Trait that lifts an intraprocedural analysis into a bottom-up, compositional interprocedural analysis. Here, the type Summary represents a transformation of the final data flow analysis state.

Required Methods

fn to_summary(
    &self,
    state: Self::State,
    fun_target: &FunctionTarget<'_>
) -> Summary

Specifies mapping from elements of dataflow analysis domain to elements of Domain.

Provided Methods

fn summarize(
    &self,
    fun_target: &FunctionTarget<'_>,
    initial_state: Self::State
) -> Summary

Computes a postcondition for the function data and then maps the postcondition to an element of abstract domain Domain by applying to_summary function. The result is stored in the summary cache of data.

Implementors