creusot_contracts/std/
io.rs

1use crate::prelude::*;
2use std::fmt;
3
4extern_spec! {
5    mod std {
6        mod io {
7            /// This is an implementation detail of `std`: we specify it so that we can use
8            /// `print!` and `println!`.
9            #[check(terminates)]
10            #[ensures(true)]
11            fn _print(args: fmt::Arguments<'_>) {}
12
13            /// This is an implementation detail of `std`: we specify it so that we can use
14            /// `eprint!` and `eprintln!`.
15            #[check(terminates)]
16            #[ensures(true)]
17            fn _eprint(args: fmt::Arguments<'_>) {}
18        }
19    }
20}