Adjust tests

creusot-rs · Dec 23, 2024 · f554cd0 · f554cd0
1 parent 49e0863
commit f554cd0
Show file tree

Hide file tree

Showing 12 changed files with 18 additions and 39 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<T>
            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
@@ -10,8 +10,6 @@ error[E0308]: mismatched types
   = help: consider constraining the associated type `<i128 as creusot_contracts::View>::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
@@ -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