Add a guard that checks the AST_UTILS_REQUESTS table against the plug-in's actual registration - #15
Merged
Conversation
dead_code cannot fire on a pub item in a pub mod, which is what every item in src/ became when the unit tests moved out of the crate. The guard that replaced the lint parsed pub fn, pub async fn and pub unsafe fn and nothing else: 313 of the 482 published items. The other 140, the pub structs, consts, enums and types, were covered by the lint on one side and by the guard on the other, so by neither.
self_check probes a hand-written table, and every count assertion over it read the table's own length, so they compared the constant against itself. A plug-in too old to register a name passed self_check and then failed at the tool. The table stays hand-written because it also carries the probed flag, which is this server's policy rather than the plug-in's. The name and the command verb are the plug-in's, so those two columns are compared against the OCaml source. Verified against the runtime as well: a -server-doc dump of the loaded plug-in lists the same 28 requests with the same 28 kinds. The kind is compared because a table saying Get where the plug-in registers EXEC sends the wrong verb and fails at the tool with self_check green, which is the same failure class as a missing name. AST_UTILS_REQUESTS and AstUtilsSpec are pub so the Rust side reads the constant instead of parsing selfcheck.rs back out as text. Only the OCaml half has to be text, because cargo test --test unit runs without Frama-C.
jserv
changed the title
![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.
The drift test read one directory level of ast-utils/src, so a registration below it was skipped in silence while the comment above promised every module. rust_files already walked recursively, so this generalizes it to source_files(dir, extension, out) and routes the .ml scan through it. Reported on PR #15. Three more things the same walker was getting wrong, all of them the shape this file exists against, a guard that reports on the part of the tree it happened to reach: It swallowed a read_dir error and returned what it had. The non-empty assertions at the call sites do not catch that, because one readable directory at the top satisfies them. It panics now, naming the directory, and so does every read_to_string beside it. It returned read_dir order, which left the ast-utils site sorting afterwards and the other two reporting offenders in arbitrary order, against the contract sorted_files states eighty lines above. Each directory is sorted inside the walk, which is also right for the caller that appends two roots and counts the boundary between them. ci_named_tests_still_exist and no_em_dash_in_a_rust_comment carried two more hand-rolled recursive walkers with the tolerant behaviour, so the file stated one rule and implemented two. Both go through source_files. rust_sources keeps its own tolerance on purpose: it is called on tests/<target>/ paths that need not exist. A duplicate registration blamed whichever site lost the insert, decided by path order rather than by which one is new, so a nested duplicate pointed at a file that had been correct for months. Both sites are named now, and the drift messages carry the site too. The window comment claimed overshooting could not read the next registration's name "because the window stops before it". It does not stop; it is a fixed seven lines. What makes it safe is spacing, and the closest pair in the plug-in is seventeen lines apart, so the comment says that instead.
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
Closes a gap in the dead-code guard so it now covers all published items, not just functions, and adds a guard that checks the
AST_UTILS_REQUESTStable against the plug-in's actual registrations.pubitem (structs, consts, enums, types, static, trait, union) instead of onlyfnvariants.AST_UTILS_REQUESTSis nowpub; a new test compares its request names and command verbs against the OCaml plug-in source, walking.mlfiles recursively, catching drift that would pass self_check but fail at runtime.RemoveAnnotationParams,HoareAnalyzeParams, andGetHoareTraceParams.Written for commit b62a64f. Summary will update on new commits.