Trait move_bytecode_verifier::absint::AbstractInterpreter

pub trait AbstractInterpreter: TransferFunctions {
    fn analyze_function(
        &mut self, 
        initial_state: Self::State, 
        function_view: &FunctionView<'_>
    ) -> InvariantMap<Self::State, Self::AnalysisError> { ... }
    fn execute_block(
        &mut self, 
        block_id: BlockId, 
        pre_state: &Self::State, 
        function_view: &FunctionView<'_>
    ) -> Result<Self::State, Self::AnalysisError> { ... }
}

Provided methods

fn analyze_function(
    &mut self,
    initial_state: Self::State,
    function_view: &FunctionView<'_>
) -> InvariantMap<Self::State, Self::AnalysisError>

Analyze procedure local@function_view starting from pre-state local@initial_state.

fn execute_block(
    &mut self,
    block_id: BlockId,
    pre_state: &Self::State,
    function_view: &FunctionView<'_>
) -> Result<Self::State, Self::AnalysisError>

Implementors