Trait bytecode::compositional_analysis::CompositionalAnalysis

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

    // Provided method
    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