creusot_std/std/
fmt.rs

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

creusot_std/std/
fmt.rs
