Conversation
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.
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.
![cubic-dev-ai[bot]](https://avatars.githubusercontent.com/in/1082092?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary by cubic
Splits glued closing
*/markers in Frama-C ACSL annotations onto their own line, and fixes the packer deleting a rule run stranded at a paragraph's end.ACSL closer handling
*/onto its own line, aligned under the opener's*, while keeping every token of the annotation intact.@*/.Rule borrowing fix
Written for commit dd3cf07. Summary will update on new commits.