Method initialize

language/move-prover/bytecode/src/verification_analysis.rs:229–348

(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder)

    }

    fn initialize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
        let options = ProverOptions::get(env);

        // If we are verifying only one function or module, check that this indeed exists.
        match &options.verify_scope {
            VerificationScope::Only(name) | VerificationScope::OnlyModule(name) => {
                let for_module = matches!(&options.verify_scope, VerificationScope::OnlyModule(_));
                let mut target_exists = false;
                for module in env.get_modules() {
                    if module.is_target() {
                        if for_module {
                            target_exists = module.matches_name(name)
                        } else {
                            target_exists = module.get_functions().any(|f| f.matches_name(name));
                        }
                        if target_exists {
                            break;
                        }
                    }
                }
                if !target_exists {
                    env.error(
                        &env.unknown_loc(),
                        &format!(
                            "{} target {} does not exist in target modules",
                            if for_module { "module" } else { "function" },
                            name
                        ),
                    )
                }
            }
            _ => {}
        }

        // Collect information for global invariant instrumentation

        // probe how global invariants will be evaluated in the functions
        let (fun_set_with_inv_check_on_exit, fun_set_with_no_inv_check) =
            Self::probe_invariant_status_in_functions(env);

        // get a map on how invariants are applicable in functions
        let fun_to_inv_map = Self::build_function_to_invariants_map(env, targets);

        // error checking, this needs to be done after the invariant applicability map because some
        // rules depends on information in that map.
        for fun_id in &fun_set_with_no_inv_check {
            let fun_env = env.get_function(*fun_id);

            // Rule 1: external-facing functions are not allowed in the N set (i.e., have invariant
            // checking completely turned-off), UNLESS they don't modify any memory that are checked
            // in any suspendable invariant.
            if fun_env.has_unknown_callers() {
                let relevance = fun_to_inv_map.get(fun_id).unwrap();
                let num_suspendable_inv_modified = relevance
                    .modified
                    .iter()
                    .filter(|inv_id| is_invariant_suspendable(env, **inv_id))
                    .count();