Skip to content

Commit 4860011

Browse files
zjp-CNzjp-CN
committed
debug(span_to_source): source_callsite, parent_callsite, and macro_backtrace
[find_oldest_ancestor_in_same_ctxt] inner!($name, $block) [source_callsite] outer! { proof2, { assert_eq!(kani::any::<u8>(), 0) }} [parent_callsite] inner!($name, $block) [macro_backtrace - callsite] inner!($name, $block) [macro_backtrace - defsite ] macro_rules! inner { ($name:ident, $block:block) => { #[kani::proof] fn $name() $block } } [macro_backtrace - callsite] outer! { proof2, { assert_eq!(kani::any::<u8>(), 0) }} [macro_backtrace - defsite ] macro_rules! outer { ($name:ident, $block:block) => { inner!($name, $block); }; } [find_oldest_ancestor_in_same_ctxt] trivial_arbitrary!(u8) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] trivial_arbitrary!(u8) [macro_backtrace - callsite] trivial_arbitrary!(u8) [macro_backtrace - defsite ] macro_rules! trivial_arbitrary { ( $type: ty ) => { impl Arbitrary for $type { #[inline(always)] fn any() -> Self { // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. unsafe { crate::kani::any_raw_internal::<Self>() } } fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] { unsafe { crate::kani::any_raw_array::<Self, MAX_ARRAY_LENGTH>() } } } }; } [macro_backtrace - callsite] kani_core::generate_arbitrary!(std) [macro_backtrace - defsite ] macro_rules! generate_arbitrary [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] kani_core::kani_intrinsics!(std) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - defsite ] macro_rules! kani_intrinsics [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] kani_core::kani_intrinsics!(std) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - defsite ] macro_rules! kani_intrinsics [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] kani_core::kani_intrinsics!(std) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - defsite ] macro_rules! kani_intrinsics [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] kani_core::kani_intrinsics!(std) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - defsite ] macro_rules! kani_intrinsics [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] kani_core::kani_intrinsics!(std) [source_callsite] kani_core::kani_lib!(kani) [parent_callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - callsite] kani_core::kani_intrinsics!(std) [macro_backtrace - defsite ] macro_rules! kani_intrinsics [macro_backtrace - callsite] kani_core::kani_lib!(kani) [macro_backtrace - defsite ] macro_rules! kani_lib [find_oldest_ancestor_in_same_ctxt] inner!($name, $block) [source_callsite] outer! { proof1, { assert_eq!(kani::any::<u8>(), 0) }} [parent_callsite] inner!($name, $block) [macro_backtrace - callsite] inner!($name, $block) [macro_backtrace - defsite ] macro_rules! inner { ($name:ident, $block:block) => { #[kani::proof] fn $name() $block } } [macro_backtrace - callsite] outer! { proof1, { assert_eq!(kani::any::<u8>(), 0) }} [macro_backtrace - defsite ] macro_rules! outer { ($name:ident, $block:block) => { inner!($name, $block); }; } [find_oldest_ancestor_in_same_ctxt] inner!($name, $block) [source_callsite] outer! { proof3, { assert_eq!(kani::any::<u8>(), 1) }} [parent_callsite] inner!($name, $block) [macro_backtrace - callsite] inner!($name, $block) [macro_backtrace - defsite ] macro_rules! inner { ($name:ident, $block:block) => { #[kani::proof] fn $name() $block } } [macro_backtrace - callsite] outer! { proof3, { assert_eq!(kani::any::<u8>(), 1) }} [macro_backtrace - defsite ] macro_rules! outer { ($name:ident, $block:block) => { inner!($name, $block); }; }
1 parent 2aaf703 commit 4860011

File tree

1 file changed

+16
-1
lines changed

1 file changed

+16
-1
lines changed

‎src/functions/utils.rs‎

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ fn span_to_source(span: Span, src_map: &SourceMap) -> String {
6262
src_map
6363
.span_to_source(span, |text, x, y| {
6464
let src = &text[x..y];
65-
debug!("[{x}:{y}]\n{src}");
65+
// debug!("[{x}:{y}]\n{src}");
6666
Ok(src.to_owned())
6767
})
6868
.unwrap()
@@ -79,6 +79,21 @@ pub fn source_code_with(
7979
let span = internal(tcx, stable_mir_span);
8080
let src = span_to_source(span, src_map);
8181
let before_expansion = span.from_expansion().then(|| {
82+
{
83+
debug!(
84+
"[find_oldest_ancestor_in_same_ctxt] {}",
85+
span_to_source(span.find_oldest_ancestor_in_same_ctxt(), src_map)
86+
);
87+
debug!("[source_callsite] {}", span_to_source(span.source_callsite(), src_map));
88+
if let Some(parent_callsite) = span.parent_callsite() {
89+
debug!("[parent_callsite] {}", span_to_source(parent_callsite, src_map));
90+
}
91+
for m in span.macro_backtrace() {
92+
debug!("[macro_backtrace - callsite] {}", span_to_source(m.call_site, src_map));
93+
debug!("[macro_backtrace - defsite ] {}", span_to_source(m.def_site, src_map));
94+
}
95+
debug!("\n");
96+
}
8297
let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
8398
span_to_source(ancestor_span, src_map)
8499
});

0 commit comments

Comments
 (0)