Require any function with a tait in its signature to actually constra… · model-checking/verify-rust-std@63fe960 (original) (raw)
`@@ -428,39 +428,43 @@ impl fmt::Display for Backtrace {
`
428
428
`}
`
429
429
`}
`
430
430
``
431
``
`-
type LazyResolve = impl (FnOnce() -> Capture) + Send + Sync + UnwindSafe;
`
432
``
-
433
``
`-
fn lazy_resolve(mut capture: Capture) -> LazyResolve {
`
434
``
`-
move || {
`
435
``
`-
// Use the global backtrace lock to synchronize this as it's a
`
436
``
`` -
// requirement of the backtrace crate, and then actually resolve
``
437
``
`-
// everything.
`
438
``
`-
let _lock = lock();
`
439
``
`-
for frame in capture.frames.iter_mut() {
`
440
``
`-
let symbols = &mut frame.symbols;
`
441
``
`-
let frame = match &frame.frame {
`
442
``
`-
RawFrame::Actual(frame) => frame,
`
443
``
`-
#[cfg(test)]
`
444
``
`-
RawFrame::Fake => unimplemented!(),
`
445
``
`-
};
`
446
``
`-
unsafe {
`
447
``
`-
backtrace_rs::resolve_frame_unsynchronized(frame, |symbol| {
`
448
``
`-
symbols.push(BacktraceSymbol {
`
449
``
`-
name: symbol.name().map(|m| m.as_bytes().to_vec()),
`
450
``
`-
filename: symbol.filename_raw().map(|b| match b {
`
451
``
`-
BytesOrWideString::Bytes(b) => BytesOrWide::Bytes(b.to_owned()),
`
452
``
`-
BytesOrWideString::Wide(b) => BytesOrWide::Wide(b.to_owned()),
`
453
``
`-
}),
`
454
``
`-
lineno: symbol.lineno(),
`
455
``
`-
colno: symbol.colno(),
`
``
431
`+
mod helper {
`
``
432
`+
use super::*;
`
``
433
`+
pub(super) type LazyResolve = impl (FnOnce() -> Capture) + Send + Sync + UnwindSafe;
`
``
434
+
``
435
`+
pub(super) fn lazy_resolve(mut capture: Capture) -> LazyResolve {
`
``
436
`+
move || {
`
``
437
`+
// Use the global backtrace lock to synchronize this as it's a
`
``
438
`` +
// requirement of the backtrace crate, and then actually resolve
``
``
439
`+
// everything.
`
``
440
`+
let _lock = lock();
`
``
441
`+
for frame in capture.frames.iter_mut() {
`
``
442
`+
let symbols = &mut frame.symbols;
`
``
443
`+
let frame = match &frame.frame {
`
``
444
`+
RawFrame::Actual(frame) => frame,
`
``
445
`+
#[cfg(test)]
`
``
446
`+
RawFrame::Fake => unimplemented!(),
`
``
447
`+
};
`
``
448
`+
unsafe {
`
``
449
`+
backtrace_rs::resolve_frame_unsynchronized(frame, |symbol| {
`
``
450
`+
symbols.push(BacktraceSymbol {
`
``
451
`+
name: symbol.name().map(|m| m.as_bytes().to_vec()),
`
``
452
`+
filename: symbol.filename_raw().map(|b| match b {
`
``
453
`+
BytesOrWideString::Bytes(b) => BytesOrWide::Bytes(b.to_owned()),
`
``
454
`+
BytesOrWideString::Wide(b) => BytesOrWide::Wide(b.to_owned()),
`
``
455
`+
}),
`
``
456
`+
lineno: symbol.lineno(),
`
``
457
`+
colno: symbol.colno(),
`
``
458
`+
});
`
456
459
`});
`
457
``
`-
});
`
``
460
`+
}
`
458
461
`}
`
459
``
`-
}
`
460
462
``
461
``
`-
capture
`
``
463
`+
capture
`
``
464
`+
}
`
462
465
`}
`
463
466
`}
`
``
467
`+
use helper::*;
`
464
468
``
465
469
`impl RawFrame {
`
466
470
`fn ip(&self) -> *mut c_void {
`