check_for_checkpoint

rapx::verify::smt_check::init

Function check_for_checkpoint 

Source 
pub(crate) fn check_for_checkpoint<'tcx>(
    checker: &SmtChecker<'tcx>,
    caller: DefId,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult
Expand description

Check Init at a return checkpoint for struct invariant verification.