creusot_std/std/
panicking.rs

1use crate::prelude::*;
2#[cfg(all(creusot, feature = "std"))]
3use core::any::Any;
4#[cfg(creusot)]
5use core::{fmt, panicking::AssertKind};
6
7extern_spec! {
8    mod core {
9        mod panicking {
10            #[check(ghost)]
11            #[requires(false)]
12            fn panic(expr: &'static str) -> !;
13
14            #[check(ghost)]
15            #[requires(false)]
16            fn panic_display<T: fmt::Display>(x: &T) -> !;
17
18            #[check(ghost)]
19            #[requires(false)]
20            fn panic_fmt(fmt: fmt::Arguments<'_>) -> !;
21
22            #[check(ghost)]
23            #[requires(false)]
24            fn panic_nounwind(expr: &'static str) -> !;
25
26            #[check(ghost)]
27            #[requires(false)]
28            fn panic_nounwind_fmt(fmt: fmt::Arguments<'_>, force_no_backtrace: bool) -> !;
29
30            #[check(ghost)]
31            #[requires(false)]
32            fn panic_nounwind_nobacktrace(expr: &'static str) -> !;
33
34            #[check(ghost)]
35            #[requires(false)]
36            fn unreachable_display<T: fmt::Display>(x: &T) -> !;
37
38            #[check(ghost)]
39            #[requires(false)]
40            fn assert_failed<T, U>(kind: AssertKind, left: &T, right: &U, args: Option<fmt::Arguments<'_>>) -> !
41            where
42                T: fmt::Debug + ?Sized,
43                U: fmt::Debug + ?Sized;
44
45        }
46    }
47}
48
49#[cfg(feature = "std")]
50extern_spec! {
51    mod std {
52        mod rt {
53            #[check(ghost)]
54            #[requires(false)]
55            fn begin_panic<M: Any + Send>(msg: M) -> !;
56        }
57    }
58}
creusot_std/std/panicking.rs

creusot_std/std/
panicking.rs
