(
&self,
targets: &mut FunctionTargetsHolder,
fun_env: &FunctionEnv<'_>,
mut data: FunctionData,
)
| 82 | |
| 83 | impl FunctionTargetProcessor for VerificationAnalysisProcessor { |
| 84 | fn process( |
| 85 | &self, |
| 86 | targets: &mut FunctionTargetsHolder, |
| 87 | fun_env: &FunctionEnv<'_>, |
| 88 | mut data: FunctionData, |
| 89 | ) -> FunctionData { |
| 90 | // This function implements the logic to decide whether to verify this function |
| 91 | |
| 92 | // Rule 1: never verify if "pragma verify = false;" |
| 93 | if !fun_env.is_pragma_true(VERIFY_PRAGMA, || true) { |
| 94 | return data; |
| 95 | } |
| 96 | |
| 97 | // Rule 2: verify the function if it is within the target modules |
| 98 | let env = fun_env.module_env.env; |
| 99 | let target_modules = env.get_target_modules(); |
| 100 | |
| 101 | let is_in_target_module = target_modules |
| 102 | .iter() |
| 103 | .any(|menv| menv.get_id() == fun_env.module_env.get_id()); |
| 104 | if is_in_target_module { |
| 105 | if Self::is_within_verification_scope(fun_env) { |
| 106 | Self::mark_verified(fun_env, &mut data, targets); |
| 107 | } |
| 108 | return data; |
| 109 | } |
| 110 | |
| 111 | // Rule 3: verify the function if a global invariant (including update invariant) that is |
| 112 | // defined in the target modules (a.k.a. a target invariant) need to be checked in the |
| 113 | // function, i.e., the function directly modifies some memory that are covered by at least |
| 114 | // one of the target invariants. |
| 115 | let inv_analysis = env.get_extension::<InvariantAnalysisData>().unwrap(); |
| 116 | let target_invs: BTreeSet<_> = target_modules |
| 117 | .iter() |
| 118 | .map(|menv| env.get_global_invariants_by_module(menv.get_id())) |
| 119 | .flatten() |
| 120 | .collect(); |
| 121 | let inv_relevance = inv_analysis |
| 122 | .fun_to_inv_map |
| 123 | .get(&fun_env.get_qualified_id()) |
| 124 | .unwrap(); |
| 125 | if !inv_relevance.direct_modified.is_disjoint(&target_invs) { |
| 126 | if Self::is_within_verification_scope(fun_env) { |
| 127 | Self::mark_verified(fun_env, &mut data, targets); |
| 128 | } |
| 129 | return data; |
| 130 | } |
| 131 | |
| 132 | // we don't verify this function |
| 133 | data |
| 134 | } |
| 135 | |
| 136 | fn name(&self) -> String { |
| 137 | "verification_analysis".to_string() |
nothing calls this directly
no test coverage detected