diff --git a/creusot/tests/should_fail/array.stderr b/creusot/tests/should_fail/array.stderr index a293ca296..c0950e6c4 100644 --- a/creusot/tests/should_fail/array.stderr +++ b/creusot/tests/should_fail/array.stderr @@ -10,7 +10,5 @@ error: Unsupported expression: Repeat 13 | #[requires([0; 4] == x)] | ^^^^^^ -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors diff --git a/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr index 01b2dacef..8e6180ce3 100644 --- a/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot add `i32` to `i32` in logic = help: the trait `creusot_contracts::logic::ops::AddLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::AddLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr index 45664c967..6681f2a30 100644 --- a/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot divide `i32` by `i32` in logic = help: the trait `creusot_contracts::logic::ops::DivLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::DivLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr index cd3e64dc8..0d9323a41 100644 --- a/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr @@ -12,8 +12,6 @@ error[E0599]: no method named `index_logic` found for struct `S` in the current candidate #1: `creusot_contracts::logic::ops::IndexLogic` = note: this error originates in the attribute macro `logic` (in Nightly builds, run with -Z macro-backtrace for more info) -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error For more information about this error, try `rustc --explain E0599`. diff --git a/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr index 65db425a2..b64d56939 100644 --- a/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot multiply `i32` by `i32` in logic = help: the trait `creusot_contracts::logic::ops::MulLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::MulLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr index e9cebb84b..352b211c3 100644 --- a/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: cannot apply unary operator `-` to type `i32` = help: the trait `creusot_contracts::logic::ops::NegLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::NegLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr index d528fdc4d..7eb868a10 100644 --- a/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: cannot calculate the remainder of `i32` divided by `i32` in logic = help: the trait `creusot_contracts::logic::ops::RemLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::RemLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr index 5f8b3c2da..d35cf3838 100644 --- a/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot subtract `i32` from `i32` in logic = help: the trait `creusot_contracts::logic::ops::SubLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::SubLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.rs b/creusot/tests/should_fail/diagnostics/view_unimplemented.rs index 3d78f330a..5c61fe293 100644 --- a/creusot/tests/should_fail/diagnostics/view_unimplemented.rs +++ b/creusot/tests/should_fail/diagnostics/view_unimplemented.rs @@ -7,8 +7,9 @@ struct S; #[logic] fn views(x: S) { let _ = x.view(); +} + +fn view_operator(x: S) { // FIXME(diagnostics): this error is printed twice, why? let _ = pearlite! { x@ }; } - -// FIXME(diagnostics): separating this into 2 functions causes the second one to be ignored. We probably have an early exit that is a bit too eager (Look into the "Cannot fetch THIR body" error). diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr index 15b406d9b..7c2f27fcf 100644 --- a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr @@ -22,9 +22,9 @@ note: the trait `creusot_contracts::View` must be implemented candidate #1: `creusot_contracts::View` error[E0277]: Cannot take the model of `S` - --> view_unimplemented.rs:11:25 + --> view_unimplemented.rs:14:25 | -11 | let _ = pearlite! { x@ }; +14 | let _ = pearlite! { x@ }; | ^- | | | no implementation for `S@` @@ -43,9 +43,9 @@ error[E0277]: Cannot take the model of `S` and 32 others error[E0277]: Cannot take the model of `S` - --> view_unimplemented.rs:11:25 + --> view_unimplemented.rs:14:25 | -11 | let _ = pearlite! { x@ }; +14 | let _ = pearlite! { x@ }; | ^^ no implementation for `S@` | = help: the trait `creusot_contracts::View` is not implemented for `S` @@ -60,9 +60,7 @@ error[E0277]: Cannot take the model of `S` creusot_contracts::Snapshot and 32 others -error: internal error: Cannot fetch THIR body - -error: aborting due to 4 previous errors +error: aborting due to 3 previous errors Some errors have detailed explanations: E0277, E0599. For more information about an error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/non_bool_assertion.stderr b/creusot/tests/should_fail/non_bool_assertion.stderr index 1a0729a8b..e6d9baeee 100644 --- a/creusot/tests/should_fail/non_bool_assertion.stderr +++ b/creusot/tests/should_fail/non_bool_assertion.stderr @@ -10,8 +10,6 @@ error[E0308]: mismatched types = help: consider constraining the associated type `::ViewTy` to `bool` = note: for more information, visit https://doc.rust-lang.org/book/ch19-03-advanced-traits.html -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error For more information about this error, try `rustc --explain E0308`. diff --git a/creusot/tests/should_fail/unsupported/macros.stderr b/creusot/tests/should_fail/unsupported/macros.stderr index c2e3aa76d..78198e2ac 100644 --- a/creusot/tests/should_fail/unsupported/macros.stderr +++ b/creusot/tests/should_fail/unsupported/macros.stderr @@ -4,7 +4,5 @@ error: Unsupported expression: macros other than `pearlite!` or `proof_assert!` 7 | panic!() | ^^^^^^^^ -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error