Skip to content

Commit a537bff

Browse files
committed
chore: inspect span.find_oldest_ancestor_in_same_ctxt()
cc #31 (comment) $ cargo r -- --json=false tests/proofs/gen_by_macros.rs ... (stable_mir span to internal span) [tests/proofs/gen_by_macros.rs:4:9: 4:26 (#4)] fn $name() $block [src/functions/mod.rs:114:5] span.from_expansion() = true [src/functions/mod.rs:114:5] ancestor_span.from_expansion() = false (find_oldest_ancestor_in_same_ctxt) [tests/proofs/gen_by_macros.rs:10:5: 10:57 (#0)] gen! { proof1, { assert_eq!(kani::any::<u8>(), 0) }} (stable_mir span to internal span) [/home/zjp/rust/distributed-verification/kani/library/kani_core/src/arbitrary.rs:38:21: 41:22 (#32)] 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>() } } [src/functions/mod.rs:114:5] span.from_expansion() = true [src/functions/mod.rs:114:5] ancestor_span.from_expansion() = true (find_oldest_ancestor_in_same_ctxt) [/home/zjp/rust/distributed-verification/kani/library/kani_core/src/arbitrary.rs:66:9: 66:31 (#5)] trivial_arbitrary!(u8) ...
1 parent d95bf1c commit a537bff

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

src/functions/mod.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,18 @@ fn ty_to_fndef(ty: Ty) -> Option<FnDef> {
105105

106106
/// Source code for a span.
107107
fn source_code(span: Span, src_map: &SourceMap) -> String {
108+
// println!("{span:?}\n{:?}\n\n", span.find_oldest_ancestor_in_same_ctxt());
109+
_ = src_map.span_to_source(span, |text, x, y| {
110+
println!("(stable_mir span to internal span) [{span:?}]\n{}", &text[x..y]);
111+
Ok(())
112+
});
113+
let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
114+
dbg!(span.from_expansion(), ancestor_span.from_expansion());
115+
_ = src_map.span_to_source(ancestor_span, |text, x, y| {
116+
println!("(find_oldest_ancestor_in_same_ctxt) [{ancestor_span:?}]\n{}\n\n", &text[x..y]);
117+
Ok(())
118+
});
119+
108120
src_map
109121
.span_to_source(span, |text, x, y| {
110122
let src = &text[x..y];

0 commit comments

Comments
 (0)