Skip to content

Commit

Permalink
Fix bug where successful selective verification is still cached
Browse files Browse the repository at this point in the history
In general, when skipping verification, we introduced a so called
fake_error to make sure the compiler does not just cache this
as successful verification and then skip later verifications even
if that's not intended. Same issue occured for selective verification,
when verifying a single method that is "correct", this would be cached.
Now we throw a fake error in this case too, to avoid this.
  • Loading branch information
cedihegi committed Feb 25, 2023
1 parent 2cc9233 commit d7cd97a
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 5 deletions.
10 changes: 7 additions & 3 deletions prusti/src/callbacks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -152,20 +152,24 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
procedures: annotated_procedures,
types,
};
verify(env, def_spec, verification_task);
verify(&env, def_spec, verification_task);
} else {
let target_def_path = config::selective_verify().unwrap();
let procedures = annotated_procedures
.into_iter()
.filter(|x| env.name.get_unique_item_name(*x) == target_def_path)
.collect();
let selective_task = VerificationTask { procedures, types };
verify(env, def_spec, selective_task);
// fake_error because otherwise a verification-success
// (for a single method for example) will cause this result
// to be cached by compiler at the moment
verify(&env, def_spec, selective_task);
fake_error(&env);
}
} else if config::show_ide_info() && config::skip_verification() && !config::no_verify()
{
// add a fake error, reason explained in issue #1261
fake_error(env)
fake_error(&env)
}
});

Expand Down
2 changes: 1 addition & 1 deletion prusti/src/ide_helper/fake_error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use prusti_rustc_interface::{errors::MultiSpan, span::DUMMY_SP};
/// when we just collect information for prusti-assistant), because then
/// a successful result will be cached and subsequent actual verifications succeed
/// (see issue #1261)
pub fn fake_error(env: Environment) {
pub fn fake_error(env: &Environment) {
let sp = MultiSpan::from_span(DUMMY_SP);
let message = String::from("[Prusti: FakeError]");
let help = None;
Expand Down
2 changes: 1 addition & 1 deletion prusti/src/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use prusti_interface::{
use prusti_viper::verifier::Verifier;

pub fn verify<'tcx>(
env: Environment<'tcx>,
env: &Environment<'tcx>,
def_spec: typed::DefSpecificationMap,
verification_task: VerificationTask<'tcx>,
) {
Expand Down

0 comments on commit d7cd97a

Please sign in to comment.