creusot_std/std/
fmt.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::fmt::{Debug, Result};
4
5extern_spec! {
6    impl<'a> core::fmt::Formatter<'a> {
7        #[requires(true)]
8        fn write_str(&mut self, data: &str) -> Result;
9
10        #[requires(true)]
11        fn debug_struct_field1_finish<'b>(
12            &'b mut self,
13            name: &str,
14            name1: &str,
15            value1: &dyn Debug,
16        ) -> Result;
17
18        #[requires(true)]
19        fn debug_struct_field2_finish<'b>(
20            &'b mut self,
21            name: &str,
22            name1: &str,
23            value1: &dyn Debug,
24            name2: &str,
25            value2: &dyn Debug,
26        ) -> Result;
27
28        #[requires(true)]
29        fn debug_struct_field3_finish<'b>(
30            &'b mut self,
31            name: &str,
32            name1: &str,
33            value1: &dyn Debug,
34            name2: &str,
35            value2: &dyn Debug,
36            name3: &str,
37            value3: &dyn Debug,
38        ) -> Result;
39
40        #[requires(true)]
41        fn debug_struct_field4_finish<'b>(
42            &'b mut self,
43            name: &str,
44            name1: &str,
45            value1: &dyn Debug,
46            name2: &str,
47            value2: &dyn Debug,
48            name3: &str,
49            value3: &dyn Debug,
50            name4: &str,
51            value4: &dyn Debug,
52        ) -> Result;
53
54        #[requires(true)]
55        fn debug_struct_field5_finish<'b>(
56            &'b mut self,
57            name: &str,
58            name1: &str,
59            value1: &dyn Debug,
60            name2: &str,
61            value2: &dyn Debug,
62            name3: &str,
63            value3: &dyn Debug,
64            name4: &str,
65            value4: &dyn Debug,
66            name5: &str,
67            value5: &dyn Debug,
68        ) -> Result;
69
70        #[requires(true)]
71        fn debug_struct_fields_finish<'b>(
72            &'b mut self,
73            name: &str,
74            names: &[&str],
75            values: &[&dyn Debug],
76        ) -> Result;
77
78        #[requires(true)]
79        fn debug_tuple_field1_finish<'b>(
80            &'b mut self,
81            name: &str,
82            value1: &dyn Debug,
83        ) -> Result;
84
85        #[requires(true)]
86        fn debug_tuple_field2_finish<'b>(
87            &'b mut self,
88            name: &str,
89            value1: &dyn Debug,
90            value2: &dyn Debug,
91        ) -> Result;
92
93        #[requires(true)]
94        fn debug_tuple_field3_finish<'b>(
95            &'b mut self,
96            name: &str,
97            value1: &dyn Debug,
98            value2: &dyn Debug,
99            value3: &dyn Debug,
100        ) -> Result;
101
102        #[requires(true)]
103        fn debug_tuple_field4_finish<'b>(
104            &'b mut self,
105            name: &str,
106            value1: &dyn Debug,
107            value2: &dyn Debug,
108            value3: &dyn Debug,
109            value4: &dyn Debug,
110        ) -> Result;
111
112        #[requires(true)]
113        fn debug_tuple_field5_finish<'b>(
114            &'b mut self,
115            name: &str,
116            value1: &dyn Debug,
117            value2: &dyn Debug,
118            value3: &dyn Debug,
119            value4: &dyn Debug,
120            value5: &dyn Debug,
121        ) -> Result;
122
123        #[requires(true)]
124        fn debug_tuple_fields_finish<'b>(
125            &'b mut self,
126            name: &str,
127            values: &[&dyn Debug],
128        ) -> Result;
129    }
130}
131
132extern_spec! {
133    impl<'a> core::fmt::Arguments<'a> {
134        #[check(ghost)]
135        fn from_str(s: &'static str) -> Self;
136    }
137}
creusot_std/std/fmt.rs

creusot_std/std/
fmt.rs
