Skip to content

Commit

Permalink
Update rustc to nightly-2022-01-13
Browse files Browse the repository at this point in the history
  • Loading branch information
@Aurel300
Aurel300 committed Jan 13, 2022
1 parent f7f3e1b commit b88c872
Show file tree
Hide file tree
Showing 37 changed files with 322 additions and 356 deletions.
348 changes: 155 additions & 193 deletions Cargo.lock
View file

Large diffs are not rendered by default.

11 changes: 6 additions & 5 deletions analysis/src/domains/definitely_accessible/state.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ fn pretty_print_place<'tcx>(
variant = Some(variant_index);
}
mir::ProjectionElem::Field(field, field_ty) => {
let field_name = describe_field_from_ty(prev_ty, field, variant)?;
let field_name = describe_field_from_ty(tcx, prev_ty, field, variant)?;
pieces.push(format!(".{})", field_name));
prev_ty = field_ty;
variant = None;
Expand All @@ -234,13 +234,14 @@ fn pretty_print_place<'tcx>(

/// End-user visible description of the `field_index`nth field of `ty`
fn describe_field_from_ty(
tcx: TyCtxt<'_>,
ty: ty::Ty<'_>,
field: mir::Field,
variant_index: Option<VariantIdx>,
) -> Option<String> {
if ty.is_box() {
// If the type is a box, the field is described from the boxed type
describe_field_from_ty(ty.boxed_ty(), field, variant_index)
describe_field_from_ty(tcx, ty.boxed_ty(), field, variant_index)
} else {
match *ty.kind() {
ty::TyKind::Adt(def, _) => {
Expand All @@ -250,14 +251,14 @@ fn describe_field_from_ty(
} else {
def.non_enum_variant()
};
Some(variant.fields[field.index()].ident.to_string())
Some(variant.fields[field.index()].ident(tcx).to_string())
}
ty::TyKind::Tuple(_) => Some(field.index().to_string()),
ty::TyKind::Ref(_, ty, _) | ty::TyKind::RawPtr(ty::TypeAndMut { ty, .. }) => {
describe_field_from_ty(ty, field, variant_index)
describe_field_from_ty(tcx, ty, field, variant_index)
}
ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) => {
describe_field_from_ty(ty, field, variant_index)
describe_field_from_ty(tcx, ty, field, variant_index)
}
ty::TyKind::Closure(..) | ty::TyKind::Generator(..) => {
// Supporting these cases is complex
Expand Down
6 changes: 3 additions & 3 deletions prusti-interface/src/environment/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,9 +278,9 @@ impl<'tcx> Environment<'tcx> {
/// Get all relevant trait declarations for some type.
pub fn get_traits_decls_for_type(&self, ty: &ty::Ty<'tcx>) -> HashSet<DefId> {
let mut res = HashSet::new();
let traits = self.tcx().all_traits(());
for trait_id in traits.iter() {
self.tcx().for_each_relevant_impl(*trait_id, ty, |impl_id| {
let traits = self.tcx().all_traits();
for trait_id in traits {
self.tcx().for_each_relevant_impl(trait_id, ty, |impl_id| {
if let Some(relevant_trait_id) = self.tcx().trait_id_of_impl(impl_id) {
res.insert(relevant_trait_id);
}
Expand Down
1 change: 1 addition & 0 deletions prusti-specs/src/specifications/common.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -367,6 +367,7 @@ impl<EID: Clone + Debug, ET: Clone + Debug, AT: Clone + Debug> ProcedureSpecific
///
/// In other words, any pre-/post-condition provided by `other` will overwrite any provided by
/// `self`.
#[must_use]
pub fn refine(&self, other: &Self) -> Self {
let pres = if other.pres.is_empty() {
self.pres.clone()
Expand Down
12 changes: 6 additions & 6 deletions prusti-specs/src/specifications/untyped.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,17 +235,17 @@ impl AssignExpressionId<TriggerSet> for common::TriggerSet<(), syn::Expr> {
spec_id: SpecificationId,
id_generator: &mut ExpressionIdGenerator,
) -> TriggerSet {
TriggerSet {
0: self.0
common::TriggerSet(
self.0
.into_iter()
.map(|x| common::Trigger {
0: x.0
.map(|x| common::Trigger(
x.0
.into_iter()
.map(|y| y.assign_id(spec_id, id_generator))
.collect()
})
))
.collect()
}
)
}
}

Expand Down
2 changes: 1 addition & 1 deletion prusti-tests/tests/cargo_verify/prusti_toml/output.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ fn prusti_post_item_test1_[..](result: ()) {
|| -> bool { false };
}
#[prusti::post_spec_id_ref = "[..]"]
pub fn test1() { }
pub fn test1() {}
pub fn test2() {
if !false { ::core::panicking::panic("assertion failed: false") };
}
Expand Down
8 changes: 4 additions & 4 deletions prusti-tests/tests/parse/ui/after_expiry.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ fn prusti_post_item_test1_$(NUM_UUID)(a: bool,
}
#[prusti::pledge_spec_id_ref =
"$(NUM_UUID):$(NUM_UUID)"]
fn test1(a: bool) { }
fn test1(a: bool) {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -69,7 +69,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(a: bool,
}
#[prusti::pledge_spec_id_ref =
"$(NUM_UUID):$(NUM_UUID)"]
fn test2(a: bool) { }
fn test2(a: bool) {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -83,7 +83,7 @@ fn prusti_post_item_test3_$(NUM_UUID)(a: bool,
|| -> bool { a };
}
#[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"]
fn test3(a: bool) { }
fn test3(a: bool) {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -97,7 +97,7 @@ fn prusti_post_item_test4_$(NUM_UUID)(a: bool,
|| -> bool { a };
}
#[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"]
fn test4(a: bool) { }
fn test4(a: bool) {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down
10 changes: 5 additions & 5 deletions prusti-tests/tests/parse/ui/and.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test1() { }
fn test1() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -53,7 +53,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test2() { }
fn test2() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -74,7 +74,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test3() { }
fn test3() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -95,7 +95,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test4() { }
fn test4() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -120,7 +120,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test5() { }
fn test5() {}
fn main() {}
Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:6 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#1}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:10 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#1}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:12 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#2}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
Expand Down
42 changes: 21 additions & 21 deletions prusti-tests/tests/parse/ui/composite.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test1() { }
fn test1() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -85,7 +85,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test2() { }
fn test2() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -106,7 +106,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test3() { }
fn test3() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -131,7 +131,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test4() { }
fn test4() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -160,7 +160,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() {
|| -> bool { true || true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test5() { }
fn test5() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -193,7 +193,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test6() { }
fn test6() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -226,7 +226,7 @@ fn prusti_pre_item_test7_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test7() { }
fn test7() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -243,7 +243,7 @@ fn prusti_pre_item_test8_$(NUM_UUID)() {
|| -> bool { true || true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test8() { }
fn test8() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -260,7 +260,7 @@ fn prusti_pre_item_test9_$(NUM_UUID)() {
|| -> bool { true || (true && (true || true)) };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test9() { }
fn test9() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -283,7 +283,7 @@ fn prusti_pre_item_test10_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test10() { }
fn test10() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -302,7 +302,7 @@ fn prusti_pre_item_test12_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test12() { }
fn test12() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -329,7 +329,7 @@ fn prusti_pre_item_test13_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test13() { }
fn test13() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -352,7 +352,7 @@ fn prusti_pre_item_test14_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test14() { }
fn test14() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -375,7 +375,7 @@ fn prusti_pre_item_test15_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test15() { }
fn test15() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -408,7 +408,7 @@ fn prusti_pre_item_test16_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test16() { }
fn test16() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -431,7 +431,7 @@ fn prusti_pre_item_test17_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test17() { }
fn test17() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -450,7 +450,7 @@ fn prusti_pre_item_test19_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test19() { }
fn test19() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -477,7 +477,7 @@ fn prusti_pre_item_test20_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test20() { }
fn test20() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -500,7 +500,7 @@ fn prusti_pre_item_test21_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test21() { }
fn test21() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand All @@ -523,7 +523,7 @@ fn prusti_pre_item_test22_$(NUM_UUID)() {
|| -> bool { true };
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test22() { }
fn test22() {}
#[allow(unused_must_use, unused_variables, dead_code)]
#[prusti::spec_only]
#[prusti::spec_id = "$(NUM_UUID)"]
Expand Down Expand Up @@ -556,7 +556,7 @@ fn prusti_pre_item_test23_$(NUM_UUID)() {
};
}
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test23() { }
fn test23() {}
fn main() {}
Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:99 ~ composite[$(CRATE_ID)]::prusti_pre_item_test19_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:67 ~ composite[$(CRATE_ID)]::prusti_pre_item_test12_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
Expand Down
Loading

0 comments on commit b88c872

Please sign in to comment.