From 86794bdd21fc5b9dc61599da576d5ae0244225c2 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Mon, 31 Aug 2026 21:41:02 +0800 Subject: [PATCH 1/3] Split a glued ACSL closer onto its own line A multi-line Frama-C ACSL annotation whose closing "*/" is glued to the last clause now gets that "*/" moved down. The annotation body is parser-visible syntax and stays byte for byte; only the closer's line moves, which is layout, since Frama-C reads whitespace as whitespace and the multi-line form is spelled with "*/" alone on the last line. Checked against Frama-C 33: "frama-c -print" is byte-identical across the move for a real contract, for a body whose last line ends in an ACSL "//" comment, and for a ghost block. This rides the branch that already split a trailing block's closer, so split_trailing_block_closer grew an indent override. Reusing the last line's own indentation is right for a "*"-marked block and wrong here: an annotation has no "*" markers and hangs its clauses under the "/*@ " text column, so the closer would land mid-line. It takes the comment's own indent plus one space instead, putting "*/" under the opener's "*". force_passthrough is one bit standing for several unrelated reasons, so being an ACSL annotation does not mean ACSL is why the comment is pinned. Each other reason keeps its veto: a bare CR still makes any rewrite unsafe, since every visual line after the first is inside the node, and a cppcheck suppression on an interior line still pins the comment on its own rail. The other two directive rails cannot co-occur with "/*@" at all, because both read the first line and strip only "/" and "*" off it, so the "@" survives and their keyword match never fires. A closer already spelled "@*/" is left alone. Splint rides the same "/*@" prefix and "@*/" is its required delimiter, so splitting it deletes the delimiter outright; the same spelling is the idiomatic "@"-marker ACSL closer, where splitting only strands a bare "@". One rule covers both. Trailing annotations are excluded too, since their line_indent_bytes is empty and the closer would land at column 1. The language gate is load-bearing rather than defensive: a Rust nested "/*@ outer /* inner */ more; */" and an assembly "/*@" carrying a bare CR are the two ways a non-C comment reaches the branch, and both would be rewritten without it. --- README.md | 6 ++- src/lib.rs | 31 +++++++++---- src/normalize.rs | 42 +++++++++++------- src/parse.rs | 44 +++++++++++++++++++ tests/convergence.rs | 11 +++++ tests/pipeline.rs | 102 ++++++++++++++++++++++++++++++++++++++----- 6 files changed, 200 insertions(+), 36 deletions(-) diff --git a/README.md b/README.md index d6b7b67..cf38d71 100644 --- a/README.md +++ b/README.md @@ -40,7 +40,11 @@ Tool directives stay intact. `// clang-format off`, `// NOLINT`, `cppcheck-suppress`, Frama-C ACSL `/*@ ... */`, `// IWYU pragma:`, `# shellcheck disable=`, `/// cbindgen:`, and similar directives are machine instructions, not prose. Reflowing one can move it away from the line it guards, -so these comments pass through untouched. +so these comments pass through untouched. The one layout fix applied to a +multi-line Frama-C ACSL block is moving a glued closing `*/` onto its own line, +under the opener's `*`; the annotation body itself stays byte for byte. A +closer already spelled `@*/` is left alone, since that is Splint's required +delimiter and the idiomatic `@`-marker ACSL closer. No build context required. Parsing is Tree-sitter-based, so each file is analyzed on its own. There are no translation units, include paths, diff --git a/src/lib.rs b/src/lib.rs index cec0c04..ca923f6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -268,15 +268,28 @@ pub fn plan( } let kind = classify::classify(&c.text, lang); let Some(doc) = normalize::normalize(c, &kind, lang, column_limit) else { - // Trailing block comments skip reflow, but a glued closing "*/" on - // the last line still gets split onto its own line. - if !c.force_passthrough - && c.is_trailing - && matches!( - kind.style, - classify::Style::Block | classify::Style::DocBlock - ) - && let Some(text) = normalize::split_trailing_block_closer(&c.text) + // Two kinds of block comment skip reflow but still get a glued + // closing "*/" split onto its own line: trailing blocks, and ACSL + // annotations. An ACSL body is parser-visible syntax that must stay + // byte-identical (see "is_acsl_annotation"), but the closer's line + // is pure layout: Frama-C reads whitespace as whitespace, and the + // multi-line form is spelled with "*/" alone on the last line. The + // closer lands under the opener's "*" rather than under the clause + // column, which is where the last line's own indent would put it. + // "acsl_closer_split_allowed" holds the guards: every OTHER reason + // a comment can be pinned as passthrough still vetoes the split. + let closer_indent = if parse::acsl_closer_split_allowed(source, c, lang) { + Some(format!("{} ", c.line_indent_bytes)) + } else if !c.force_passthrough && c.is_trailing { + None + } else { + continue; + }; + if matches!( + kind.style, + classify::Style::Block | classify::Style::DocBlock + ) && let Some(text) = + normalize::split_trailing_block_closer(&c.text, closer_indent.as_deref()) && let Some(replacement) = rewrite::make_replacement(c, text, source) { out.push(replacement); diff --git a/src/normalize.rs b/src/normalize.rs index 2b14a89..5ae1d26 100644 --- a/src/normalize.rs +++ b/src/normalize.rs @@ -193,11 +193,16 @@ pub fn normalize( /// "normalize"), but a multi-line one whose closing "*/" is glued to the last /// content line still reads badly, and clang-format won't move it. This is the /// one layout fix applied to trailing blocks: split a glued "*/" onto its own -/// line, reusing the last line's indentation (which lands "*/" under the -/// continuation "*" marker when one is present, else under the content). -/// Returns the comment text, or "None" when there is nothing to split +/// line. Returns the comment text, or "None" when there is nothing to split /// (single-line, "*/" already alone, or no content before the closer). -pub fn split_trailing_block_closer(text: &str) -> Option { +/// +/// "closer_indent" is the indentation for the new closer line. "None" reuses +/// the last line's own indentation, which lands "*/" under the continuation +/// "*" marker when one is present, else under the content. An ACSL annotation +/// has no "*" markers and indents its clauses under the "/*@ " text column, so +/// that rule would park the closer mid-line; the caller passes the comment's +/// own indent plus one space instead, putting "*/" under the opener's "*". +pub fn split_trailing_block_closer(text: &str, closer_indent: Option<&str>) -> Option { let nl = text.rfind('\n')?; let (prefix, last_line) = (&text[..=nl], &text[nl + 1..]); @@ -215,10 +220,13 @@ pub fn split_trailing_block_closer(text: &str) -> Option { return None; } - let indent: String = last_line - .chars() - .take_while(|&c| c == ' ' || c == '\t') - .collect(); + let indent: String = match closer_indent { + Some(i) => i.to_string(), + None => last_line + .chars() + .take_while(|&c| c == ' ' || c == '\t') + .collect(), + }; let eol = if prefix.ends_with("\r\n") { "\r\n" } else { @@ -733,9 +741,9 @@ fn is_param_xref(word: &str, param_names: &[&str]) -> bool { kdoc_xref_name(word).is_some_and(|name| param_names.contains(&name) && doxy_tag(name).is_none()) } -/// The parameter name an "@name"/"\\name" cross-reference points at, or "None" if the -/// word cannot be one. Trailing punctuation is trimmed, since a reference at a -/// clause break ("@align,") is still a reference. +/// The parameter name an "@name"/"\\name" cross-reference points at, or "None" +/// if the word cannot be one. Trailing punctuation is trimmed, since a +/// reference at a clause break ("@align,") is still a reference. /// /// Both Doxygen spellings are supported, except one-character C escapes such /// as "\\n"; the name must otherwise open like a C identifier, so "\\0" @@ -1245,21 +1253,21 @@ mod tests { // the continuation stars. let text = "/* foo\n * bar. */"; assert_eq!( - split_trailing_block_closer(text).as_deref(), + split_trailing_block_closer(text, None).as_deref(), Some("/* foo\n * bar.\n */") ); // Idempotent: an already-split closer is left alone. assert_eq!( - split_trailing_block_closer("/* foo\n * bar.\n */"), + split_trailing_block_closer("/* foo\n * bar.\n */", None), None ); // Single-line trailing block has no interior line to split. - assert_eq!(split_trailing_block_closer("/* foo */"), None); + assert_eq!(split_trailing_block_closer("/* foo */", None), None); // Empty last line (bare closer with only a marker) stays put. - assert_eq!(split_trailing_block_closer("/* foo\n * */"), None); + assert_eq!(split_trailing_block_closer("/* foo\n * */", None), None); // CRLF endings are preserved. assert_eq!( - split_trailing_block_closer("/* foo\r\n * bar. */").as_deref(), + split_trailing_block_closer("/* foo\r\n * bar. */", None).as_deref(), Some("/* foo\r\n * bar.\r\n */") ); } @@ -1342,6 +1350,7 @@ mod tests { // Escape sequences and names beginning with a digit are not references. assert_eq!(kdoc_xref_name("\\n"), None); assert_eq!(kdoc_xref_name("\\0"), None); + // Trailing punctuation must not smuggle an escape past the check: a // clause ends with "\\n." as readily as it ends with "\\n". assert_eq!(kdoc_xref_name("\\n."), None); @@ -1352,6 +1361,7 @@ mod tests { assert_eq!(kdoc_xref_name("@0"), None); assert_eq!(kdoc_xref_name("@"), None); assert_eq!(kdoc_xref_name("plain"), None); + // A path shape is not a reference even though it opens with a tag // keyword: the dot leaves "file.txt" outside the identifier grammar. assert_eq!(kdoc_xref_name("@file.txt"), None); diff --git a/src/parse.rs b/src/parse.rs index e484290..b86a961 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -675,6 +675,50 @@ pub(crate) fn is_passthrough_directive(text: &str, lang: Language) -> bool { || is_lint_directive(text, lang) } +/// True when a comment is pinned as passthrough for the ACSL reason and *only* +/// that reason, and its closing "*/" may be moved onto its own line. +/// +/// "force_passthrough" is one bit standing for several unrelated reasons, so +/// "this is an ACSL annotation" does not mean "ACSL is why it is pinned". A +/// bare CR still makes any rewrite unsafe (every visual line after the first is +/// inside the node, so the emitted text is not what it looks like), and an +/// annotation carrying a cppcheck suppression on an interior line is pinned by +/// that suppression too. Each reason keeps its own veto. +/// +/// The other two directive rails cannot co-occur with ACSL and are not tested +/// for: "is_formatter_directive" and "is_lint_directive" both read the FIRST +/// line, and both strip only "/" and "*" off it, so the "@" of "/*@" survives +/// and their keyword match can never fire on an annotation. Only cppcheck's +/// rail scans every line, which is what puts it within reach. +/// +/// The last line must carry real annotation text before the "*/", and the +/// closer must not be spelled "@*/". Splint annotations ride the same "/*@" +/// prefix and "@*/" is Splint's REQUIRED closing delimiter, so splitting it +/// deletes the delimiter; the same spelling is the idiomatic "@"-marker ACSL +/// closer, where splitting only strands a bare "@" on a line of its own. One +/// rule covers both: a closer that already carries its marker is left alone. +/// +/// Trailing annotations are excluded. "line_indent_bytes" is empty for a +/// comment that shares its line with code, so the closer would land at column 1 +/// instead of under the opener's "*". +pub(crate) fn acsl_closer_split_allowed(source: &str, c: &Comment, lang: Language) -> bool { + if !matches!(lang, Language::C | Language::Cpp) || !is_acsl_annotation(&c.text) { + return false; + } + if c.is_trailing + || spans_bare_cr(source, c.start_byte, c.end_byte) + || is_cppcheck_suppress(&c.text) + { + return false; + } + let last = c.text.rsplit('\n').next().unwrap_or("").trim_end(); + if last.ends_with("@*/") { + return false; + } + last.strip_suffix("*/") + .is_some_and(|before| !before.trim().trim_matches(['@', '*']).is_empty()) +} + fn is_verbatim_open(trimmed: &str) -> bool { ["@code", "\\code", "@verbatim", "\\verbatim"] .iter() diff --git a/tests/convergence.rs b/tests/convergence.rs index 567fa57..8a5037c 100644 --- a/tests/convergence.rs +++ b/tests/convergence.rs @@ -171,6 +171,17 @@ fn shapes(body: &str) -> Vec<(&'static str, String)> { ("foo.rs", format!("fn f() {{}}\n// {body}\n")), ("foo.sh", format!("f() {{ :; }}\n# {body}\n")), ("foo.S", format!("nop\n/* {body} */\n")), + // ACSL, both closer spellings. The glued "*/" is split onto its own + // line and must land on a fixed point; the "@*/" form is vetoed and + // must come back byte-identical. + ( + "foo.c", + format!("/*@ requires x;\n {body} */\nint f(void);\n"), + ), + ( + "foo.c", + format!("/*@ requires x;\n @ {body}\n @*/\nint f(void);\n"), + ), ] } diff --git a/tests/pipeline.rs b/tests/pipeline.rs index 6a259c0..7fd6a67 100644 --- a/tests/pipeline.rs +++ b/tests/pipeline.rs @@ -112,10 +112,91 @@ fn pipeline_skips_rust_nested_block() { } #[test] -fn pipeline_skips_frama_c_acsl_annotations() { +fn pipeline_skips_frama_c_acsl_bodies() { let src = "/*@ requires n >= 0;\n @ assigns \\nothing;\n @ ensures \\result >= 0;\n */\nint f(int n);\n//@ assert x >= 0;\n"; let out = pipeline(src, detect("foo.c"), 30); - assert_eq!(src, out, "ACSL annotations must stay byte-identical"); + assert_eq!(src, out, "an ACSL body must stay byte-identical"); +} + +#[test] +fn pipeline_splits_glued_acsl_closer() { + // The annotation body is parser-visible syntax and must survive verbatim; + // only the glued "*/" moves, landing under the opener's "*". + let src = "/*@ requires \\valid(p);\n assigns *p; */\nvoid f(int *p);\n"; + let out = pipeline(src, detect("foo.c"), 80); + assert_eq!( + out, "/*@ requires \\valid(p);\n assigns *p;\n */\nvoid f(int *p);\n", + "a glued ACSL closer moves to its own line" + ); + // Indented annotation: the closer follows the comment's own indent. + let src = " /*@ assigns *p;\n ensures *p == 0; */\n"; + let out = pipeline(src, detect("foo.c"), 80); + assert_eq!( + out, " /*@ assigns *p;\n ensures *p == 0;\n */\n", + "closer sits under the opener's \"*\"" + ); +} + +#[test] +fn pipeline_keeps_glued_acsl_closer_when_another_rail_applies() { + // Splint rides the same "/*@" prefix and "@*/" is its required closing + // delimiter; the same spelling is the idiomatic "@"-marker ACSL closer. + let src = "/*@\n modifies x; @*/\nint x;\n"; + assert_eq!( + pipeline(src, detect("foo.c"), 80), + src, + "\"@*/\" is left alone" + ); + let src = "/*@ requires x > 0;\n @ ensures \\result > 0;\n @*/\nint f(int x);\n"; + assert_eq!( + pipeline(src, detect("foo.c"), 80), + src, + "\"@*/\" is left alone" + ); + + // A bare CR pins the comment whatever else it is: every visual line after + // the first is inside the node, so no rewrite is safe. + let src = "/*@ requires p;\r ensures q;\n assigns z; */\nint g(void);\n"; + assert_eq!( + pipeline(src, detect("foo.c"), 80), + src, + "bare CR still vetoes" + ); + + // Trailing annotation: "line_indent_bytes" is empty, so the closer would + // land at column 1 rather than under the opener's "*". + let src = "int x; /*@\n ensures x == 0; */\n"; + assert_eq!( + pipeline(src, detect("foo.c"), 80), + src, + "trailing ACSL untouched" + ); + + // An interior cppcheck suppression pins the annotation on its own rail. The + // other two directive rails read the FIRST line and strip only "/" and "*" + // off it, so the "@" of "/*@" survives and they can never fire here. + let src = "/*@ requires x;\n cppcheck-suppress nullPointer\n ensures y; */\nint a;\n"; + assert_eq!( + pipeline(src, detect("foo.c"), 80), + src, + "interior cppcheck suppression still vetoes" + ); + + // The language gate is load-bearing, not defensive: these are the two ways + // a non-C comment opening with "/*@" reaches the branch at all, via + // "rust_block_has_nested" and "spans_bare_cr". + let src = "/*@ outer /* inner */\n more; */\nfn f() {}\n"; + assert_eq!( + pipeline(src, detect("foo.rs"), 80), + src, + "a Rust nested block is not an annotation" + ); + let src = "/*@ a\r b; */\n.text\n"; + assert_eq!( + pipeline(src, detect("foo.S"), 80), + src, + "assembly has no ACSL rail" + ); } #[test] @@ -924,8 +1005,9 @@ fn kernel_doc_entry_hangs_its_continuations_under_the_description() { // the same way a "@param" entry does. Shape from tlsf-bsd's tlsf.h. let src = "/**\n * @prev : Pointer to the previous physical block. Only valid when the previous block is free; physically stored at the tail of that block's payload.\n * @header : Size or status bits.\n */\nstruct b { int prev; };\n"; let out = pipeline(src, detect("foo.c"), 80); - // Assert the column rather than a hardcoded run of spaces: the - // continuation must begin exactly under "Pointer". + + // Assert the column rather than a hardcoded run of spaces: the continuation + // must begin exactly under "Pointer". let lines: Vec<&str> = out.lines().collect(); let head = lines.iter().position(|l| l.contains("@prev :")).unwrap(); let desc_col = lines[head].find("Pointer").unwrap(); @@ -943,10 +1025,10 @@ fn kernel_doc_entry_hangs_its_continuations_under_the_description() { #[test] fn packer_never_forges_a_kernel_doc_tag_mid_paragraph() { - // A lone "@buf" that takes a ":"-led word on a continuation line would be - // a tag line the source never had. "classify_lines" splits a paragraph at - // one, so the next pass regroups the text and the hanging indent moves - // with it. The harness's second-pass assertion is the real test here. + // A lone "@buf" that takes a ":"-led word on a continuation line would be a + // tag line the source never had. "classify_lines" splits a paragraph at + // one, so the next pass regroups the text and the hanging indent moves with + // it. The harness's second-pass assertion is the real test here. let src = "/**\n * alpha beta gamma delta epsilon zeta eta theta iota kappa @buf : lambda mu\n */\nint f(int buf);\n"; let out = pipeline(src, detect("foo.c"), 46); assert!( @@ -958,8 +1040,8 @@ fn packer_never_forges_a_kernel_doc_tag_mid_paragraph() { #[test] fn packer_never_splits_a_kernel_doc_entry_from_its_colon() { // The mirror: a name long enough to fill the opening line must still keep - // its ":" , overflowing if it has to. A first line ending at "@name" is - // not a tag line on the next pass, so the entry would dissolve. + // its ":" , overflowing if it has to. A first line ending at "@name" is not + // a tag line on the next pass, so the entry would dissolve. let src = "/**\n * lead words here\n * @destination_buffer_length : alpha beta gamma delta epsilon\n */\nint f(int destination_buffer_length);\n"; let out = pipeline(src, detect("foo.c"), 34); assert!( From cd2dae6ea91f247514527cdf81007f370b6e9097 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Mon, 31 Aug 2026 21:41:43 +0800 Subject: [PATCH 2/3] Borrow across a stranded rule at a paragraph's end The packer must never emit a line a later pass rewrites. At a paragraph's end it may be holding a bookend, and it had exactly one escape: borrow the last word of the line above. That escape fails on a rule-led line, where both of its tests fire at once. On "-------- \result @1buf:" with "***" left over, the single word available to borrow is a kernel-doc tag, which may not open a line, and the "--------" that taking it leaves behind is a bare rule, which may not stand alone. The arm then fell through and emitted the rule by itself, and the next pass read that as a bare rule and deleted it. A lost word, which is the failure this tool exists to avoid. Every split point in the line above is now tried, longest prefix first, so a borrow can take two words or more; and when the only cut that frees a non-tag opener strands a bare rule, that run folds onto the line above it instead of standing alone. The case above packs as "@param.txt @1buf --------" over "\result @1buf: ***", two lines nothing downstream rewrites. The tag test also reads the whole borrowed segment through is_kernel_doc_tag now, not just its first word, which catches the spaced "@name : desc" form the single-word test could not see. The bug was pre-existing and reachable from the committed vocabulary; the fixed seed simply never arranged those words that way. Widening VOCAB for the ACSL closer shapes reshuffled the packing and hit it, which is the argument for widening rather than for hand-written cases. The three words are back, along with the two ACSL shapes. only_a_tag_or_a_rule_may_overflow needed its predicate corrected as well. It asserted an overlong line ends in a tag or a rule word, but the mid-paragraph guard escapes a two-sided bookend by appending a word past the trailing run, so the line legitimately ends in whatever word broke it. That packing is pre-existing and byte-identical with this change reverted; the vocabulary could not generate it before. --- src/reflow.rs | 78 +++++++++++++++++++++++++++++++++++++------- tests/convergence.rs | 24 +++++++++++--- tests/pipeline.rs | 24 ++++++++++++++ 3 files changed, 111 insertions(+), 15 deletions(-) diff --git a/src/reflow.rs b/src/reflow.rs index c7fdc3e..99ede07 100644 --- a/src/reflow.rs +++ b/src/reflow.rs @@ -611,25 +611,81 @@ fn wrap_segment_aligned( .unwrap_or(&out[last]) .to_string(); - // The borrowed word opens the paragraph's last line, and that line is + // The borrowed text opens the paragraph's last line, and that line is // always a continuation, so the tag rule above applies to it just as it // does to a mid-paragraph break: a tag parked at the first column is // read by "classify_lines" as its own tag paragraph, the next pass // regroups around it, and the hanging indent moves with the regrouping. // - // When there is nothing to borrow, or borrowing would build one of the + // Every split point is tried, longest prefix first, so the borrow can + // take two words or more. Borrowing exactly one is not enough on a line + // that carries rule runs, and that is the line this arm sees most: the + // one word above the rule is often a tag, which may not open a line, + // while the prefix left behind by taking it is often a bare rule, which + // may not stand alone. Both fire at once on "-------- \result @1buf:", + // where the only safe cut is two words up. Taking the single-word split + // as the whole search emitted the rule alone, and the next pass read + // that as a bare rule and deleted it, losing a word. + // + // When nothing can be borrowed, or every borrow builds one of the // shapes above, fold the rule onto the line above whole. That arm used // to sit inside the "there is a word to borrow" case, so a line holding // ONE word (no space to split at) fell through and emitted the rule - // alone anyway, which the next pass reads as a bare rule and deletes. - let borrow = prev_body.rfind(' ').filter(|&space| { - let borrowed = &prev_body[space + 1..]; - !is_tag_start(borrowed) - && bookend_match(&prev_body[..space]).is_none() - && bookend_match(&format!("{borrowed} {current}")).is_none() - }); - if let Some(space) = borrow { - out[last] = format!("{prev_prefix}{}", &prev_body[..space]); + // alone anyway. + let opens_with_tag = |seg: &str| { + // "is_tag_start" reads one word; "is_kernel_doc_tag" reads a line + // start, so it also catches the spaced "@name : desc" form, whose + // first word alone ("@name") is not a tag. + is_tag_start(seg.split_whitespace().next().unwrap_or("")) || is_kernel_doc_tag(seg) + }; + + // A split is usable when the text moved down may open a line and + // neither resulting line is a bookend. The prefix left behind gets one + // extra chance: a bare rule there may be folded onto the line above it, + // which is how the rule-led case resolves. "-------- \result @1buf:" + // has no usable split on its own, since the only cut that frees a + // non-tag opener strands "--------"; folding that run one line further + // up yields "@param.txt @1buf --------" over "\result @1buf: ***", two + // lines the next pass rewrites neither of. + let above = |i: usize| { + let p = if i == first_line_mark { + prefix + } else { + cont_prefix + }; + (p, out[i].strip_prefix(p).unwrap_or(&out[i]).to_string()) + }; + let usable = prev_body + .match_indices(' ') + .map(|(space, _)| space) + .rev() + .find_map(|space| { + let borrowed = &prev_body[space + 1..]; + if opens_with_tag(borrowed) + || bookend_match(&format!("{borrowed} {current}")).is_some() + { + return None; + } + let head = &prev_body[..space]; + if bookend_match(head).is_none() { + return Some((space, false)); + } + if last <= first_line_mark { + return None; + } + let (_, above_body) = above(last - 1); + bookend_match(&format!("{above_body} {head}")) + .is_none() + .then_some((space, true)) + }); + if let Some((space, fold_head)) = usable { + if fold_head { + let (above_prefix, above_body) = above(last - 1); + out[last - 1] = format!("{above_prefix}{above_body} {}", &prev_body[..space]); + out.remove(last); + } else { + out[last] = format!("{prev_prefix}{}", &prev_body[..space]); + } current = format!("{} {current}", &prev_body[space + 1..]); } else if bookend_match(&format!("{prev_body} {current}")).is_none() { out[last] = format!("{prev_prefix}{prev_body} {current}"); diff --git a/tests/convergence.rs b/tests/convergence.rs index 8a5037c..dd44fb3 100644 --- a/tests/convergence.rs +++ b/tests/convergence.rs @@ -132,6 +132,15 @@ const VOCAB: &[&str] = &[ "========", "---", "***", + // ACSL clause shapes. The annotation body is passthrough, but its closer + // decides between split, veto, and no-op, so the words around it have to be + // generatable. A bare "@" is the continuation marker Frama-C reads as + // whitespace. "@*/" is deliberately NOT here: a body word spelling a block + // closer would terminate every block shape early, so the two closers are + // pinned in "shapes" instead. + "\\valid(p);", + "\\result", + "@", // Escapes that open with a marker but are ordinary prose. "\\0", "\\n", @@ -244,10 +253,11 @@ fn converged_output_survives_reruns() { } /// The tag rule is allowed to overrun the column limit, but only where it has -/// no other move. There are exactly two such moves, and both trade width for +/// no other move. There are exactly two such reasons, and both trade width for /// bytes: a run of tags it cannot break in front of, and a rule run it must not /// strand on its own line. Any other overlong line is a packing bug, so pin the -/// two exceptions rather than the absence of one. +/// two exceptions rather than the absence of one. The rule-run reason has two +/// spellings, since escaping a two-sided bookend appends a word past the run. #[test] fn only_a_tag_or_a_rule_may_overflow() { let mut rng = Rng(0xBEEF_0003); @@ -260,9 +270,15 @@ fn only_a_tag_or_a_rule_may_overflow() { if line.chars().count() <= width || !line.starts_with("//") { continue; } - let last = line.split_whitespace().next_back().unwrap_or(""); + let words: Vec<&str> = line.split_whitespace().collect(); + let is_rule = |w: &str| w.starts_with(['-', '=', '*']); + let last = words.last().copied().unwrap_or(""); let tag = last.starts_with('@') || last.starts_with('\\'); - let rule = last.starts_with(['-', '=', '*']); + // A rule run can end the line, or sit one word from the end: the + // packer escapes a two-sided bookend by appending one more word + // AFTER the trailing run, so the line then ends in whatever word + // broke it ("--- *** a -------- user@example.com"). + let rule = is_rule(last) || (words.len() >= 2 && is_rule(words[words.len() - 2])); assert!( tag || rule, "case {case} w={width} line over the limit ends in neither a tag nor a rule: {line:?}\n--- src\n{src}--- out\n{out}" diff --git a/tests/pipeline.rs b/tests/pipeline.rs index 7fd6a67..da4fb75 100644 --- a/tests/pipeline.rs +++ b/tests/pipeline.rs @@ -199,6 +199,30 @@ fn pipeline_keeps_glued_acsl_closer_when_another_rail_applies() { ); } +#[test] +fn paragraph_end_rule_borrows_across_a_stranded_run() { + // The paragraph's last word is a rule run, and the line above is rule-led, + // so the single-word borrow has no legal cut: taking "@1buf:" parks a + // kernel-doc tag at a line start, and the "--------" it leaves behind is a + // bare rule the next pass deletes. The borrow reaches two words up and + // folds the stranded run onto the line above it instead. "common::pipeline" + // asserts the second pass is a no-op, which is what used to fail here. + let src = "/* lead one\n *\n * @return: @return/x @param. reallyquitelongword @1buf @param: @return: @note/path gamma @2: @param.txt @1buf -------- \\result @1buf: ***\n */\n"; + let out = pipeline(src, detect("foo.c"), 27); + assert!( + out.contains("@param.txt @1buf --------"), + "the stranded rule folds onto the line above: {out}" + ); + assert!( + out.contains("\\result @1buf: ***"), + "and the rule run keeps company on the last line: {out}" + ); + assert!( + !out.lines().any(|l| l.trim() == "* ***"), + "no line is left as a bare rule for the next pass to delete: {out}" + ); +} + #[test] fn block_opener_alone_preserved() { // Source uses opener-alone form. Output must keep it that way. From dd3cf078f1bb4d77267f3a8aea633213f09e3d61 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Mon, 31 Aug 2026 21:59:43 +0800 Subject: [PATCH 3/3] Narrow the closer-split helper split_trailing_block_closer went from one argument to two, which would break any caller outside the crate. There is no such caller and there should not be: "plan" is the only one, and the closer-indent override is an implementation detail of the two rails that use it, not an API to hold still for. It is pub(crate) now, which says so, matching what the "signature" module already does. A compatibility wrapper would have kept a public shape nothing asked for. The other point is that whitespace between the last clause and a glued "*/" is dropped rather than carried along. It is, deliberately, and the promise around it was written too strongly. Leaving that gap behind would trail the emitted line with spaces, a shape this tool produces nowhere else, and the same trim has always applied on the trailing-block path, so preserving it only for ACSL would make one helper behave two ways. It costs nothing even on a rail whose bytes are otherwise untouchable: whitespace between two tokens is not a token, and Frama-C 33 prints the same AST either way. Whitespace INSIDE the body is never reached, so a ghost string literal ending in spaces keeps them. --- README.md | 8 +++++--- src/lib.rs | 6 +++--- src/normalize.rs | 32 +++++++++++++++++++++++++++++++- tests/pipeline.rs | 12 +++++++++++- 4 files changed, 50 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index cf38d71..7526803 100644 --- a/README.md +++ b/README.md @@ -42,9 +42,11 @@ Tool directives stay intact. `// clang-format off`, `// NOLINT`, instructions, not prose. Reflowing one can move it away from the line it guards, so these comments pass through untouched. The one layout fix applied to a multi-line Frama-C ACSL block is moving a glued closing `*/` onto its own line, -under the opener's `*`; the annotation body itself stays byte for byte. A -closer already spelled `@*/` is left alone, since that is Splint's required -delimiter and the idiomatic `@`-marker ACSL closer. +under the opener's `*`. Every token of the annotation survives; the only bytes +that move with the closer are the horizontal spaces that sat in front of it, +which would otherwise be left trailing the line. A closer already spelled `@*/` +is left alone, since that is Splint's required delimiter and the idiomatic +`@`-marker ACSL closer. No build context required. Parsing is Tree-sitter-based, so each file is analyzed on its own. There are no translation units, include paths, diff --git a/src/lib.rs b/src/lib.rs index ca923f6..9ef793c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -270,9 +270,9 @@ pub fn plan( let Some(doc) = normalize::normalize(c, &kind, lang, column_limit) else { // Two kinds of block comment skip reflow but still get a glued // closing "*/" split onto its own line: trailing blocks, and ACSL - // annotations. An ACSL body is parser-visible syntax that must stay - // byte-identical (see "is_acsl_annotation"), but the closer's line - // is pure layout: Frama-C reads whitespace as whitespace, and the + // annotations. An ACSL body is parser-visible syntax and no token + // of it may change (see "is_acsl_annotation"), but the closer's + // line is pure layout: Frama-C reads whitespace as whitespace, and // multi-line form is spelled with "*/" alone on the last line. The // closer lands under the opener's "*" rather than under the clause // column, which is where the last line's own indent would put it. diff --git a/src/normalize.rs b/src/normalize.rs index 5ae1d26..c5608ba 100644 --- a/src/normalize.rs +++ b/src/normalize.rs @@ -196,13 +196,29 @@ pub fn normalize( /// line. Returns the comment text, or "None" when there is nothing to split /// (single-line, "*/" already alone, or no content before the closer). /// +/// Horizontal whitespace between the last clause and the closer goes with the +/// closer: emitting it would leave the line trailing spaces, which is not a +/// shape this tool produces anywhere else, and the same trim has always applied +/// on the trailing-block path. It costs nothing even on the ACSL rail, where +/// the bytes are otherwise untouchable, because whitespace between two tokens +/// is not a token: verified against Frama-C 33, which prints the same AST +/// either way. Whitespace INSIDE the body is never reached, so a string literal +/// ending in spaces keeps them. +/// +/// Crate-private on purpose. "plan" is the only caller and the closer-indent +/// override is an implementation detail of the two rails that use it, not an +/// API to hold still for. +/// /// "closer_indent" is the indentation for the new closer line. "None" reuses /// the last line's own indentation, which lands "*/" under the continuation /// "*" marker when one is present, else under the content. An ACSL annotation /// has no "*" markers and indents its clauses under the "/*@ " text column, so /// that rule would park the closer mid-line; the caller passes the comment's /// own indent plus one space instead, putting "*/" under the opener's "*". -pub fn split_trailing_block_closer(text: &str, closer_indent: Option<&str>) -> Option { +pub(crate) fn split_trailing_block_closer( + text: &str, + closer_indent: Option<&str>, +) -> Option { let nl = text.rfind('\n')?; let (prefix, last_line) = (&text[..=nl], &text[nl + 1..]); @@ -1265,6 +1281,20 @@ mod tests { assert_eq!(split_trailing_block_closer("/* foo */", None), None); // Empty last line (bare closer with only a marker) stays put. assert_eq!(split_trailing_block_closer("/* foo\n * */", None), None); + // Whitespace between the last clause and the closer goes with the + // closer rather than being left to trail the line. + assert_eq!( + split_trailing_block_closer("/*@ requires x;\n assigns y;\t */", Some(" ")) + .as_deref(), + Some("/*@ requires x;\n assigns y;\n */") + ); + // Whitespace inside the body is never reached: a string literal that + // ends in spaces keeps them. + assert_eq!( + split_trailing_block_closer("/*@ ghost\n char *s = \"a \"; */", Some(" ")) + .as_deref(), + Some("/*@ ghost\n char *s = \"a \";\n */") + ); // CRLF endings are preserved. assert_eq!( split_trailing_block_closer("/* foo\r\n * bar. */", None).as_deref(), diff --git a/tests/pipeline.rs b/tests/pipeline.rs index da4fb75..5169448 100644 --- a/tests/pipeline.rs +++ b/tests/pipeline.rs @@ -115,7 +115,7 @@ fn pipeline_skips_rust_nested_block() { fn pipeline_skips_frama_c_acsl_bodies() { let src = "/*@ requires n >= 0;\n @ assigns \\nothing;\n @ ensures \\result >= 0;\n */\nint f(int n);\n//@ assert x >= 0;\n"; let out = pipeline(src, detect("foo.c"), 30); - assert_eq!(src, out, "an ACSL body must stay byte-identical"); + assert_eq!(src, out, "an ACSL body keeps every token"); } #[test] @@ -128,6 +128,16 @@ fn pipeline_splits_glued_acsl_closer() { out, "/*@ requires \\valid(p);\n assigns *p;\n */\nvoid f(int *p);\n", "a glued ACSL closer moves to its own line" ); + // Whitespace in front of the closer moves with it rather than being left + // to trail the line. No token changes: whitespace between two tokens is not + // one, and whitespace inside the body is never reached. + let src = "/*@ ghost\n char *s = \"a \";\t */\nvoid g(void);\n"; + let out = pipeline(src, detect("foo.c"), 80); + assert_eq!( + out, "/*@ ghost\n char *s = \"a \";\n */\nvoid g(void);\n", + "the gap before the closer goes with the closer" + ); + // Indented annotation: the closer follows the comment's own indent. let src = " /*@ assigns *p;\n ensures *p == 0; */\n"; let out = pipeline(src, detect("foo.c"), 80);