Add some impls for char

creusot-rs · Feb 27, 2025 · 9fb68c5 · 9fb68c5
1 parent 479d09b
commit 9fb68c5
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/creusot-contracts/src/std.rs b/creusot-contracts/src/std.rs
@@ -8,6 +8,7 @@ pub mod collections {
     pub mod hash_map;
     pub mod hash_set;
 }
+pub mod char;
 pub mod cmp;
 pub mod default;
 pub mod deque;

diff --git a/tests/should_fail/bug/603.stderr b/tests/should_fail/bug/603.stderr
@@ -13,7 +13,7 @@ error[E0277]: the trait bound `VecMap<K, V>: creusot_contracts::Default` is not
              (A, B, C, D)
              (A, B, C, D, E)
              (A, B, C, D, E, F)
-           and 23 others
+           and 24 others
 
 error: error above
 

diff --git a/tests/should_fail/diagnostics/view_unimplemented.stderr b/tests/should_fail/diagnostics/view_unimplemented.stderr
@@ -39,9 +39,9 @@ error[E0277]: Cannot take the model of `S`
              *mut T
              [T; N]
              [T]
+             char
              creusot_contracts::GhostBox<T>
-             creusot_contracts::Snapshot<T>
-           and 41 others
+           and 42 others
 
 error[E0277]: Cannot take the model of `S`
   --> view_unimplemented.rs:14:25
@@ -57,9 +57,9 @@ error[E0277]: Cannot take the model of `S`
              *mut T
              [T; N]
              [T]
+             char
              creusot_contracts::GhostBox<T>
-             creusot_contracts::Snapshot<T>
-           and 41 others
+           and 42 others
 
 error: aborting due to 3 previous errors