creusot_contracts/std/
panicking.rs

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

creusot_contracts/std/
panicking.rs
