Update tests

creusot-rs · Jan 16, 2025 · 05017e3 · 05017e3
1 parent 887c232
commit 05017e3
Show file tree

Hide file tree

Showing 62 changed files with 246 additions and 246 deletions.
diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma b/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma
diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr
@@ -13,9 +13,9 @@ error[E0599]: Cannot take the model of `S`
            `S: creusot_contracts::View`
            which is required by `&mut S: creusot_contracts::View`
 note: the trait `creusot_contracts::View` must be implemented
-  --> ./creusot-contracts/src/model.rs:14:1
+  --> ./creusot-contracts/src/model.rs:12:1
    |
-14 | pub trait View {
+12 | pub trait View {
    | ^^^^^^^^^^^^^^
    = help: items from traits can only be used if the trait is implemented and in scope
    = note: the following trait defines an item `view`, perhaps you need to implement it:

diff --git a/creusot/tests/should_fail/type_invariants/borrows.coma b/creusot/tests/should_fail/type_invariants/borrows.coma
diff --git a/creusot/tests/should_succeed/100doors.coma b/creusot/tests/should_succeed/100doors.coma