creusot_std/std/
io.rs

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

creusot_std/std/
io.rs
