creusot_std/std/
panicking.rs

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

creusot_std/std/
panicking.rs
