Manipulate markers in Frama-C ACSL annotations properly

README.md

@@ -40,7 +40,13 @@ 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 `*`. 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,

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 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.
+            // "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);

src/normalize.rs

@@ -193,11 +193,32 @@ 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<String> {
+///
+/// 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(crate) fn split_trailing_block_closer(
+    text: &str,
+    closer_indent: Option<&str>,
+) -> Option<String> {
     let nl = text.rfind('\n')?;
     let (prefix, last_line) = (&text[..=nl], &text[nl + 1..]);
 
@@ -215,10 +236,13 @@ pub fn split_trailing_block_closer(text: &str) -> Option<String> {
         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 +757,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 +1269,35 @@ 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);
+        // 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. */").as_deref(),
+            split_trailing_block_closer("/* foo\r\n     * bar. */", None).as_deref(),
             Some("/* foo\r\n     * bar.\r\n     */")
         );
     }
@@ -1342,6 +1380,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 +1391,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);

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()

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}");

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",
@@ -171,6 +180,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"),
+        ),
     ]
 }
 
@@ -233,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);
@@ -249,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}"