rapx 0.7.63

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

//! MIR transfer functions for the symbolic VM.

use rustc_middle::mir::{BasicBlock, Place, Rvalue, Statement, Terminator};

use super::state::{VmState, VmValue};

mod dispatch;
pub(crate) mod rvalue;
pub(crate) mod statement;
pub(crate) mod terminator;

pub(crate) fn eval_rvalue<'z3, 'tcx>(
    state: &mut VmState<'z3, 'tcx>,
    place: &Place<'tcx>,
    rvalue: &Rvalue<'tcx>,
) -> VmValue<'z3, 'tcx> {
    dispatch::eval_rvalue(state, place, rvalue)
}

pub(crate) fn exec_terminator<'z3, 'tcx>(
    state: &mut VmState<'z3, 'tcx>,
    terminator: &Terminator<'tcx>,
    switch_succ: Option<BasicBlock>,
) {
    dispatch::exec_terminator(state, terminator, switch_succ);
}

pub(crate) fn exec_statement<'z3, 'tcx>(
    state: &mut VmState<'z3, 'tcx>,
    statement: &Statement<'tcx>,
) {
    dispatch::exec_statement(state, statement);
}