Skip to content

Commit

Permalink
Erase regions in constraint solving
Browse files Browse the repository at this point in the history
  • Loading branch information
vl0w committed Apr 28, 2022
1 parent e9419cd commit 32ccf0e
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions prusti-viper/src/encoder/mir/specifications/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ use rustc_hir::def_id::{DefId, LocalDefId};
use rustc_middle::{
ty,
ty::subst::{Subst, SubstsRef},
ty::TypeFoldable,
};
use rustc_span::{MultiSpan, Span};

Expand Down Expand Up @@ -153,15 +154,18 @@ pub mod trait_bounds {
// contain a behavioral subtyping check which will be performed on the
// resolved spec.
let param_env_lookup = if let Some(caller_def_id) = context.caller_proc_def_id {
env.tcx().param_env(caller_def_id)
env.tcx().param_env_reveal_all_normalized(caller_def_id)
} else {
env.tcx().param_env(context.proc_def_id)
env.tcx().param_env_reveal_all_normalized(context.proc_def_id)
};

let all_bounds_satisfied = param_env_constraint
.caller_bounds()
.iter()
.all(|predicate| env.evaluate_predicate(predicate, param_env_lookup));
.all(|predicate| {
let predicate = env.tcx().erase_regions(predicate);
env.evaluate_predicate(predicate, param_env_lookup)
});

trace!("Constraint fulfilled: {all_bounds_satisfied}");
all_bounds_satisfied
Expand Down Expand Up @@ -228,7 +232,7 @@ pub mod trait_bounds {
.cloned()
.unwrap_or_default();
for spec_id in pres.iter().chain(posts.iter()) {
let param_env = env.tcx().param_env(spec_id.to_def_id());
let param_env = env.tcx().param_env_reveal_all_normalized(spec_id.to_def_id());
let spec_span = env.tcx().def_span(spec_id.to_def_id());
let attrs = env.tcx().get_attrs(spec_id.to_def_id());
if has_trait_bounds_ghost_constraint(attrs) {
Expand Down

0 comments on commit 32ccf0e

Please sign in to comment.