creusot_contracts/std/
fmt.rs

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

creusot_contracts/std/
fmt.rs
