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 { ... }
}
Expand description
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§
sourcefn to_summary(
&self,
state: Self::State,
fun_target: &FunctionTarget<'_>
) -> Summary
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§
sourcefn summarize(
&self,
fun_target: &FunctionTarget<'_>,
initial_state: Self::State
) -> Summary
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
.