creusot_std/std/
panicking.rs

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

creusot_std/std/
panicking.rs
