From 4fd249edcfb2e7ce1ef67a8b7c8e99c5bc0def50 Mon Sep 17 00:00:00 2001 From: fpoli Date: Fri, 15 Sep 2023 07:03:14 +0000 Subject: [PATCH] Update dependencies (rustc nightly-2023-09-15, viper v-2023-08-26-2125) --- analysis/src/bin/analysis-driver.rs | 1 - analysis/src/bin/gen-accessibility-driver.rs | 1 - .../definitely_initialized/abs.stdout | 22 ++- .../repeated_assignment.stdout | 25 ++- .../reaching_definitions/abs.stdout | 155 ++++++++++-------- .../repeated_assignment.stdout | 123 ++++++++------ .../relaxed_definitely_initialized/abs.stdout | 36 ++-- prusti-interface/src/specs/external.rs | 4 +- .../verify/ui/failing-postcondition.stderr | 4 +- .../encoder/mir/procedures/encoder/ghost.rs | 12 +- .../mir/pure/specifications/encoder_poly.rs | 6 +- prusti-viper/src/encoder/procedure_encoder.rs | 2 +- prusti/src/callbacks.rs | 3 +- rust-toolchain | 2 +- vir/defs/polymorphic/ast/common.rs | 2 +- 15 files changed, 229 insertions(+), 169 deletions(-) diff --git a/analysis/src/bin/analysis-driver.rs b/analysis/src/bin/analysis-driver.rs index 51d8f083669..75f27dd4a33 100644 --- a/analysis/src/bin/analysis-driver.rs +++ b/analysis/src/bin/analysis-driver.rs @@ -147,7 +147,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/analysis/src/bin/gen-accessibility-driver.rs b/analysis/src/bin/gen-accessibility-driver.rs index 6d0b18486d9..832d0f421e1 100644 --- a/analysis/src/bin/gen-accessibility-driver.rs +++ b/analysis/src/bin/gen-accessibility-driver.rs @@ -99,7 +99,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/analysis/tests/test_cases/definitely_initialized/abs.stdout b/analysis/tests/test_cases/definitely_initialized/abs.stdout index 02b924954e9..47c616c43a8 100644 --- a/analysis/tests/test_cases/definitely_initialized/abs.stdout +++ b/analysis/tests/test_cases/definitely_initialized/abs.stdout @@ -45,14 +45,6 @@ Result for function abs(): "_6" ], "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - [ - "_1", - "_5" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -78,6 +70,13 @@ Result for function abs(): ], "bb1": [ [ + [ + "state:", + [ + "_1" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -137,6 +136,13 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + [ + "_1" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout b/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout index c8b57b13729..87be870a5e5 100644 --- a/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout +++ b/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout @@ -131,15 +131,6 @@ Result for function main(): "_6" ], "statement: _5 = Gt(move _6, const 2_i32)" - ], - [ - "state:", - [ - "_1", - "_2", - "_5" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -168,6 +159,14 @@ Result for function main(): ], "bb2": [ [ + [ + "state:", + [ + "_1", + "_2" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -205,6 +204,14 @@ Result for function main(): ], "bb3": [ [ + [ + "state:", + [ + "_1", + "_2" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/analysis/tests/test_cases/reaching_definitions/abs.stdout b/analysis/tests/test_cases/reaching_definitions/abs.stdout index 90086fab2fe..2aab0969c4c 100644 --- a/analysis/tests/test_cases/reaching_definitions/abs.stdout +++ b/analysis/tests/test_cases/reaching_definitions/abs.stdout @@ -59,21 +59,6 @@ Result for function abs(): ] }, "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - { - "_1": [ - "arg0" - ], - "_5": [ - "bb0[5]: _5 = Ge(move _6, const 0_i32)" - ], - "_6": [ - "bb0[4]: _6 = _1" - ] - }, - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -122,6 +107,21 @@ Result for function abs(): ], "bb1": [ [ + [ + "state:", + { + "_1": [ + "arg0" + ], + "_5": [ + "bb0[5]: _5 = Ge(move _6, const 0_i32)" + ], + "_6": [ + "bb0[4]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -165,7 +165,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: _3 = move _7" @@ -177,7 +177,7 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -186,7 +186,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: StorageDead(_7)" @@ -198,7 +198,7 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -207,7 +207,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: _4 = const ()" @@ -219,10 +219,10 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_4": [ - "bb1[4]: _4 = const ()" + "bb1[5]: _4 = const ()" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -231,7 +231,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "terminator: goto -> bb4", @@ -243,10 +243,10 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_4": [ - "bb1[4]: _4 = const ()" + "bb1[5]: _4 = const ()" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -255,7 +255,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] } ] @@ -263,6 +263,21 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + { + "_1": [ + "arg0" + ], + "_5": [ + "bb0[5]: _5 = Ge(move _6, const 0_i32)" + ], + "_6": [ + "bb0[4]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -306,7 +321,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ] }, "statement: _9 = Eq(_8, const i32::MIN)" @@ -324,10 +339,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: assert(!move _9, /"attempt to negate `{}`, which would overflow/", _8) -> [success: bb3, unwind: bb5]", @@ -345,10 +360,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ], @@ -365,10 +380,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ] @@ -389,10 +404,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _3 = Neg(move _8)" @@ -413,10 +428,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_8)" @@ -437,10 +452,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _4 = const ()" @@ -464,10 +479,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: goto -> bb4", @@ -491,10 +506,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ] @@ -509,11 +524,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -523,13 +538,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_5)" @@ -541,11 +556,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -555,13 +570,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_4)" @@ -573,11 +588,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -587,13 +602,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _0 = _3" @@ -608,11 +623,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -622,13 +637,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_3)" @@ -643,11 +658,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -657,13 +672,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: return", @@ -683,10 +698,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: resume", diff --git a/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout b/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout index 32acc0cbcea..8358364481a 100644 --- a/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout +++ b/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout @@ -215,27 +215,6 @@ Result for function main(): ] }, "statement: _5 = Gt(move _6, const 2_i32)" - ], - [ - "state:", - { - "_1": [ - "bb1[0]: _1 = move _3" - ], - "_2": [ - "bb0[4]: _2 = const 3_i32" - ], - "_3": [ - "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" - ], - "_5": [ - "bb1[6]: _5 = Gt(move _6, const 2_i32)" - ], - "_6": [ - "bb1[5]: _6 = _1" - ] - }, - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -302,6 +281,27 @@ Result for function main(): ], "bb2": [ [ + [ + "state:", + { + "_1": [ + "bb1[0]: _1 = move _3" + ], + "_2": [ + "bb0[4]: _2 = const 3_i32" + ], + "_3": [ + "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" + ], + "_5": [ + "bb1[6]: _5 = Gt(move _6, const 2_i32)" + ], + "_6": [ + "bb1[5]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -330,7 +330,7 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" @@ -351,13 +351,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()" + "bb2[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -375,13 +375,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()" + "bb2[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -395,6 +395,27 @@ Result for function main(): ], "bb3": [ [ + [ + "state:", + { + "_1": [ + "bb1[0]: _1 = move _3" + ], + "_2": [ + "bb0[4]: _2 = const 3_i32" + ], + "_3": [ + "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" + ], + "_5": [ + "bb1[6]: _5 = Gt(move _6, const 2_i32)" + ], + "_6": [ + "bb1[5]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -423,7 +444,7 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" @@ -444,13 +465,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb3[1]: _4 = const ()" + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -468,13 +489,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb3[1]: _4 = const ()" + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -495,15 +516,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -521,15 +542,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -547,15 +568,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -579,8 +600,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -607,8 +628,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -635,8 +656,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -663,8 +684,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" diff --git a/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout b/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout index e5a0337d009..3aee1e2dff8 100644 --- a/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout +++ b/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout @@ -45,21 +45,13 @@ Result for function abs(): "_6" ], "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - [ - "_1", - "_5", - "_6" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", [ "_1", - "_5" + "_5", + "_6" ], "terminator: switchInt(move _5) -> [0: bb2, otherwise: bb1]", { @@ -67,20 +59,31 @@ Result for function abs(): "state:", [ "_1", - "_5" + "_5", + "_6" ] ], "bb2": [ "state:", [ "_1", - "_5" + "_5", + "_6" ] ] } ], "bb1": [ [ + [ + "state:", + [ + "_1", + "_5", + "_6" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -148,6 +151,15 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + [ + "_1", + "_5", + "_6" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/prusti-interface/src/specs/external.rs b/prusti-interface/src/specs/external.rs index 7568ed85692..0e5fc8fb1a4 100644 --- a/prusti-interface/src/specs/external.rs +++ b/prusti-interface/src/specs/external.rs @@ -177,11 +177,11 @@ impl<'tcx> ExternSpecResolver<'tcx> { let (resolved_gens, current_gens) = ( self.env_query .identity_substs(resolved_def_id) - .non_erasable_generics() + .non_erasable_generics(self.env_query.tcx(), resolved_def_id) .count(), self.env_query .identity_substs(current_def_id) - .non_erasable_generics() + .non_erasable_generics(self.env_query.tcx(), current_def_id) .count(), ); if resolved_gens != current_gens { diff --git a/prusti-tests/tests/verify/ui/failing-postcondition.stderr b/prusti-tests/tests/verify/ui/failing-postcondition.stderr index 54424aa4380..722f605d454 100644 --- a/prusti-tests/tests/verify/ui/failing-postcondition.stderr +++ b/prusti-tests/tests/verify/ui/failing-postcondition.stderr @@ -1,8 +1,8 @@ error: [Prusti: verification error] postcondition might not hold. - --> $DIR/failing-postcondition.rs:8:11 + --> $DIR/failing-postcondition.rs:8:31 | 8 | #[ensures(something_true() && false)] - | ^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^ | note: the error originates here --> $DIR/failing-postcondition.rs:9:1 diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs b/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs index 8978d1d3174..a76476ac167 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs @@ -51,12 +51,12 @@ impl<'a, 'p, 'v, 'tcx> GhostChecker<'a, 'p, 'v, 'tcx> { let ty = &self.p.mir.local_decls[*local].ty; let ty_str = format!("{ty:?}"); - let ghost_tys = ["Ghost", "Int", "Seq", "Map"]; - - for ghost in ghost_tys { - if ty_str.starts_with(&format!("prusti_contracts::{ghost}")) { - return true; - } + match &ty_str { + _ if ty_str.starts_with("Adt(prusti_contracts::Ghost,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Int,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Seq,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Map,") => return true, + _ => {} } // unit types get generated all over, and carry no information, thus okay to leak outside the ghost block diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 67f838df495..50619f97f49 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -82,12 +82,14 @@ pub(super) fn inline_spec_item<'tcx>( ) -> SpannedEncodingResult { // each non-lifetime parameter should be matched with a subst assert_eq!( - substs.non_erasable_generics().count(), + substs + .non_erasable_generics(encoder.env().tcx(), def_id) + .count(), encoder .env() .query .identity_substs(def_id) - .non_erasable_generics() + .non_erasable_generics(encoder.env().tcx(), def_id) .count() ); diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 7d0f927c43a..1d4183c5198 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2464,7 +2464,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .. } => { let ty = literal.ty(); - let func_const_val = literal.try_to_value(self.encoder.env().tcx()); + let func_const_val = literal.try_to_scalar_int(); if let ty::TyKind::FnDef(called_def_id, call_substs) = ty.kind() { let called_def_id = *called_def_id; debug!("Encode function call {:?} with substs {:?}", called_def_id, call_substs); diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index bacfd39bc3e..b622a8b1ad0 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -16,7 +16,7 @@ use prusti_rustc_interface::{ query::{ExternProviders, Providers}, ty::TyCtxt, }, - session::{EarlyErrorHandler, Session}, + session::Session, }; #[derive(Default)] @@ -134,7 +134,6 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { #[tracing::instrument(level = "debug", skip_all)] fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/rust-toolchain b/rust-toolchain index 35315b86c9c..4439ba166b4 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2023-09-01" +channel = "nightly-2023-09-15" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ] profile = "minimal" diff --git a/vir/defs/polymorphic/ast/common.rs b/vir/defs/polymorphic/ast/common.rs index 71abe8eeabb..c27081c6be5 100644 --- a/vir/defs/polymorphic/ast/common.rs +++ b/vir/defs/polymorphic/ast/common.rs @@ -95,7 +95,7 @@ impl fmt::Display for PermAmount { } } -#[allow(clippy::incorrect_partial_ord_impl_on_ord_type)] +#[allow(clippy::non_canonical_partial_ord_impl)] impl PartialOrd for PermAmount { fn partial_cmp(&self, other: &PermAmount) -> Option { match (self, other) {