Report what the front end dropped by jserv · Pull Request #16 · sysprog21/frama-c-mcp

jserv · 2026-08-30T15:33:46Z

Frama-C's front end throws things away and said so only in prose that never reached the caller. An inline-assembly memory clobber is an assumption about a statement whose real effects it cannot see; an unknown attribute is a dropped declaration. Both are points where the analyzed program stops being the compiled program, and both were invisible on the call that matters: files are parsed while Frama-C boots, before log monitoring is enabled, and getLogs before setLogs(true) returns an empty array rather than the backlog, so the first reload_project on a file carrying them answered with no messages at all.

The counts come off the spawn log instead of the message stream, which is the only record that survives that. reload_project reports them under ast_reload_health.parse_diagnostics, per category, with a capped location sample and the omitted count beside it. check turns the two soundness classes into AST_ASM_CLOBBER and AST_UNKNOWN_ATTRIBUTE, and folds every category nobody has classified into one AST_UNCLASSIFIED_WARNING entry keyed by category, because an entry per category grows with the program rather than with the finding. AST_WARNING_ALLOWLIST is the only way a category leaves that aggregate and starts empty: silence about a warning nobody has read would be this server calling it benign without saying so.

Summary by cubic

Reports what Frama-C's front end dropped during parsing. Inline-assembly clobbers and unknown attributes were invisible on reload_project and check because boot-time parse messages predate log monitoring; now both surface these gaps, including when no record establishes that the analyzed program is the compiled one.

Counts come from the spawn log, the only record that survives boot-time parsing, under ast_reload_health.parse_diagnostics per category with capped location samples; unknown attributes count per distinct name.
check maps clobbers and unknown attributes to AST_ASM_CLOBBER and AST_UNKNOWN_ATTRIBUTE, folds every other warning category into one AST_UNCLASSIFIED_WARNING entry, and reports a missing or unreadable record as AST_PARSE_DIAGNOSTICS_UNAVAILABLE.
A changed file set, edited file contents, any # in a source, or force_includes/compilation database options respawn Frama-C rather than reparse, so the record always describes a complete boot parse.
An unreadable or absent record reports an unavailable reason instead of zeros; unreadable logs are retried on the next call, while missing boot records poison the process since they can never be recovered.
AST_WARNING_ALLOWLIST starts empty; adding a category is the only way it leaves the aggregate.

^{Written for commit 1898921. Summary will update on new commits.}

cubic-dev-ai

1 issue found across 12 files (changes from recent commits).

Prompt for AI agents (unresolved issues)


Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="src/mcp/analysis.rs">

<violation number="1" location="src/mcp/analysis.rs:1624">
P1: When a reparse reports zero for a warn-once category, this branch suppresses the category entirely even though `from_initial_parse: false` means the zero is not evidence that nothing was dropped. `check` can consequently return `proved` with no AST gap; preserve an explicit uncertainty signal for zero-count categories or make the check incomplete whenever the parse record is not from the initial parse.</violation>
</file>

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai · 2026-08-30T17:27:18Z

+
+    let mut unclassified = serde_json::Map::new();
+    for (category, record) in categories {
+        if record["count"].as_u64().unwrap_or(0) == 0 {


P1: When a reparse reports zero for a warn-once category, this branch suppresses the category entirely even though from_initial_parse: false means the zero is not evidence that nothing was dropped. check can consequently return proved with no AST gap; preserve an explicit uncertainty signal for zero-count categories or make the check incomplete whenever the parse record is not from the initial parse.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/mcp/analysis.rs, line 1624: <comment>When a reparse reports zero for a warn-once category, this branch suppresses the category entirely even though `from_initial_parse: false` means the zero is not evidence that nothing was dropped. `check` can consequently return `proved` with no AST gap; preserve an explicit uncertainty signal for zero-count categories or make the check incomplete whenever the parse record is not from the initial parse.</comment> <file context> @@ -1550,6 +1557,107 @@ pub fn check_incomplete_items( + + let mut unclassified = serde_json::Map::new(); + for (category, record) in categories { + if record["count"].as_u64().unwrap_or(0) == 0 { + continue; + } </file context>

Stale as of the redesign in this branch: from_initial_parse no longer exists. The record is always a boot parse, because ensure_main_spawned respawns rather than hand back a reparse whenever it cannot prove the file set unchanged, and a spawn that could not take a boot record answers AST_PARSE_DIAGNOSTICS_UNAVAILABLE instead of zeros.

So a zero here is evidence of absence rather than a warn-once category that was already spent, which is what lets the zero-count branch stay silent. Pinned by ast_codes_do_not_depend_on_when_the_caller_asked in tests/unit/check-gaps.rs and by a_reload_counts_what_the_parse_dropped_and_keeps_counting_it over stdio.

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

2 issues found across 13 files (changes from recent commits).

Prompt for AI agents (unresolved issues)


Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="src/mcp/server.rs">

<violation number="1" location="src/mcp/server.rs:3387">
P1: When Frama-C's startup output has not reached the redirected stdout file at this point, `ast_parse_log_end` truncates the boot record and `reload_project` reports incomplete or zero parse diagnostics. Establish a flushed/stable log boundary before storing the offset, or capture the startup diagnostics through a synchronized channel.</violation>
</file>

<file name="src/mcp/project.rs">

<violation number="1" location="src/mcp/project.rs:491">
P2: When spawn-time log metadata fails, this cached arm permanently returns the unavailable record. Retry unavailable records while the process is not poisoned, so a later readable log can be parsed.</violation>
</file>

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai · 2026-08-30T20:50:46Z

+        // primed with the absence here rather than computed from a length
+        // nobody measured.
+        let (ast_parse_log_end, mut ast_reload_diagnostics) =
+            match std::fs::metadata(&stdout_log_path) {


P1: When Frama-C's startup output has not reached the redirected stdout file at this point, ast_parse_log_end truncates the boot record and reload_project reports incomplete or zero parse diagnostics. Establish a flushed/stable log boundary before storing the offset, or capture the startup diagnostics through a synchronized channel.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/mcp/server.rs, line 3387: <comment>When Frama-C's startup output has not reached the redirected stdout file at this point, `ast_parse_log_end` truncates the boot record and `reload_project` reports incomplete or zero parse diagnostics. Establish a flushed/stable log boundary before storing the offset, or capture the startup diagnostics through a synchronized channel.</comment> <file context> @@ -3201,6 +3373,38 @@ impl FramaCMcpServer { + // primed with the absence here rather than computed from a length + // nobody measured. + let (ast_parse_log_end, mut ast_reload_diagnostics) = + match std::fs::metadata(&stdout_log_path) { + Ok(metadata) => (metadata.len(), None), + Err(error) => (0, Some(project::unreadable_parse_log(&stdout_log_path, &error))), </file context>

cubic-dev-ai · 2026-08-30T20:50:46Z

+            let mut state = self.main_frama_c_state.lock().await;
+            match state.as_mut() {
+                Some(state) => match state.ast_reload_diagnostics.clone() {
+                    Some(cached) => cached,


P2: When spawn-time log metadata fails, this cached arm permanently returns the unavailable record. Retry unavailable records while the process is not poisoned, so a later readable log can be parsed.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/mcp/project.rs, line 491: <comment>When spawn-time log metadata fails, this cached arm permanently returns the unavailable record. Retry unavailable records while the process is not poisoned, so a later readable log can be parsed.</comment> <file context> @@ -235,7 +476,41 @@ impl FramaCMcpServer { + let mut state = self.main_frama_c_state.lock().await; + match state.as_mut() { + Some(state) => match state.ast_reload_diagnostics.clone() { + Some(cached) => cached, + + // A log this server cannot read is not a parse that dropped </file context>

Suggested change

Some(cached) => cached,

Some(cached) => {

if state.poisoned || cached.get("unavailable").is_none() {

cached

} else {

match read_parse_window(&state.stdout_log_path, state.ast_parse_log_end) {

Ok(log) => {

let fresh =

ast_parse_diagnostics(&log, state.ast_parse_log_end, &state.working_dir);

state.ast_reload_diagnostics = Some(fresh.clone());

fresh

}

Err(error) => unreadable_parse_log(&state.stdout_log_path, &error),

}

}

}

Addressed the other way round: the record is not retried because the process does not survive to retry it. A spawn that could not take a boot record sets poisoned (src/mcp/server.rs:3458), and the respawn decision reads that flag before anything else (src/mcp/server.rs:3258), so the next reload_project answers from a new process with its own boot parse.

Retrying would not be sound in that state. What the metadata read produces is the boundary of the boot window, a property of the instant the socket appeared. Reading the log later cannot recover it: by then the file also holds whatever EVA and WP wrote, so a re-read would either parse a window that no longer means anything or fold post-boot messages into the parse record. A new process is the only thing that produces a boot record, which is why the absence is cached and the process is replaced.

The runtime case is separate and is retried: when read_parse_window fails inside reload_project, the record is not cached and the next call reads the file again.

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 13 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

1 issue found across 14 files (changes from recent commits).

Prompt for AI agents (unresolved issues)


Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="README.md">

<violation number="1" location="README.md:459">
P2: For the "Frama-C had written nothing to its log when the socket appeared" case, the process is not replaced on the next reload_project, so the claim that "the process is replaced on the next reload_project and the code goes with it" is inaccurate. ensure_main_spawned respawns only when parse_record_survives fails (file digest/`#include`/options change); with an unchanged file set it takes the in-place branch and the cached unavailable record persists, so AST_PARSE_DIAGNOSTICS_UNAVAILABLE keeps answering. Only the "sources moved while starting" case has a digest mismatch that forces the respawn. Update the sentence to say the code resolves only when a reload triggers a respawn, and that for unchanged files the "nothing in the log" record is cached and stays on the same process.</violation>
</file>

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai · 2026-08-30T22:14:08Z

+nothing to its log when the socket appeared, or the sources moved while it was
+starting. Neither can be recovered by looking again, since the boundary they
+would need was a property of an instant that has passed, so that process is
+replaced on the next `reload_project` and the code goes with it. The third is


P2: For the "Frama-C had written nothing to its log when the socket appeared" case, the process is not replaced on the next reload_project, so the claim that "the process is replaced on the next reload_project and the code goes with it" is inaccurate. ensure_main_spawned respawns only when parse_record_survives fails (file digest/#include/options change); with an unchanged file set it takes the in-place branch and the cached unavailable record persists, so AST_PARSE_DIAGNOSTICS_UNAVAILABLE keeps answering. Only the "sources moved while starting" case has a digest mismatch that forces the respawn. Update the sentence to say the code resolves only when a reload triggers a respawn, and that for unchanged files the "nothing in the log" record is cached and stays on the same process.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At README.md, line 459: <comment>For the "Frama-C had written nothing to its log when the socket appeared" case, the process is not replaced on the next reload_project, so the claim that "the process is replaced on the next reload_project and the code goes with it" is inaccurate. ensure_main_spawned respawns only when parse_record_survives fails (file digest/`#include`/options change); with an unchanged file set it takes the in-place branch and the cached unavailable record persists, so AST_PARSE_DIAGNOSTICS_UNAVAILABLE keeps answering. Only the "sources moved while starting" case has a digest mismatch that forces the respawn. Update the sentence to say the code resolves only when a reload triggers a respawn, and that for unchanged files the "nothing in the log" record is cached and stays on the same process.</comment> <file context> @@ -427,11 +427,60 @@ payload contract and the change rule. The full set: +nothing to its log when the socket appeared, or the sources moved while it was +starting. Neither can be recovered by looking again, since the boundary they +would need was a property of an instant that has passed, so that process is +replaced on the next `reload_project` and the code goes with it. The third is +the spawn log being unreadable when a call goes to read it. That one is not +cached and not fatal: the same process answers the code for as long as its log </file context>

The README is accurate for that case. All three boot-record failures poison the process, not just the identity mismatch: ensure_main_spawned sets poisoned = ast_reload_diagnostics.is_some() (src/mcp/server.rs:3458), where that Option is exactly what boot_parse_window returns when there is no record, and the respawn decision reads s.poisoned first (src/mcp/server.rs:3258), ahead of parse_record_survives.

So an unchanged file set does not take the in-place branch after a spawn that never saw its log: the poison flag short-circuits it. The one reason that stays on the same process is the third, the log being unreadable when a call goes to read it, which is deliberately not cached and not fatal. That is the case the paragraph after this one describes.

cubic-dev-ai

1 issue found across 14 files (changes from recent commits).

Prompt for AI agents (unresolved issues)


Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="README.md">

<violation number="1" location="README.md:461">
P3: The README says the unreadable-log flavor of AST_PARSE_DIAGNOSTICS_UNAVAILABLE "is not cached and not fatal" and that "the `detail` is what says which" failure it is. That is not always true: the same "cannot read the Frama-C stdout log at ..." detail is also produced at spawn time in boot_parse_window (src/mcp/server.rs), where the unavailable record is cached in ast_reload_diagnostics and sets poisoned = ast_reload_diagnostics.is_some(), so that instance is both cached and fatal (the next reload_project respawns and drops the code). Persistence is therefore decided by where the unreadable read happens, not by the detail, so the two cases cannot be told apart by the detail as documented.</violation>
</file>

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai · 2026-08-30T22:28:10Z

+would need was a property of an instant that has passed, so the server marks
+that Frama-C unusable: the next `reload_project` replaces it whether or not the
+file set changed, and the code goes with it. The third is
+the spawn log being unreadable when a call goes to read it. That one is not


P3: The README says the unreadable-log flavor of AST_PARSE_DIAGNOSTICS_UNAVAILABLE "is not cached and not fatal" and that "the detail is what says which" failure it is. That is not always true: the same "cannot read the Frama-C stdout log at ..." detail is also produced at spawn time in boot_parse_window (src/mcp/server.rs), where the unavailable record is cached in ast_reload_diagnostics and sets poisoned = ast_reload_diagnostics.is_some(), so that instance is both cached and fatal (the next reload_project respawns and drops the code). Persistence is therefore decided by where the unreadable read happens, not by the detail, so the two cases cannot be told apart by the detail as documented.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At README.md, line 461: <comment>The README says the unreadable-log flavor of AST_PARSE_DIAGNOSTICS_UNAVAILABLE "is not cached and not fatal" and that "the `detail` is what says which" failure it is. That is not always true: the same "cannot read the Frama-C stdout log at ..." detail is also produced at spawn time in boot_parse_window (src/mcp/server.rs), where the unavailable record is cached in ast_reload_diagnostics and sets poisoned = ast_reload_diagnostics.is_some(), so that instance is both cached and fatal (the next reload_project respawns and drops the code). Persistence is therefore decided by where the unreadable read happens, not by the detail, so the two cases cannot be told apart by the detail as documented.</comment> <file context> @@ -427,11 +427,61 @@ payload contract and the change rule. The full set: +would need was a property of an instant that has passed, so the server marks +that Frama-C unusable: the next `reload_project` replaces it whether or not the +file set changed, and the code goes with it. The third is +the spawn log being unreadable when a call goes to read it. That one is not +cached and not fatal: the same process answers the code for as long as its log +stays unreadable, and starts reporting counts again as soon as it does not. </file context>

cubic-dev-ai

All reported issues were addressed across 15 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 15 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

cubic-dev-ai

All reported issues were addressed across 15 files (changes from recent commits).

_{Tip: Review your code locally with the cubic CLI to iterate faster.

Re-trigger cubic}

Frama-C's front end throws things away and said so only in prose that never reached the caller. An inline-assembly memory clobber is an assumption about a statement whose real effects it cannot see; an unknown attribute is a dropped declaration. Both are points where the analyzed program stops being the compiled program, and both were invisible on the call that matters: files are parsed while Frama-C boots, before log monitoring is enabled, and getLogs before setLogs(true) returns an empty array rather than the backlog, so the first reload_project on a file carrying them answered with no messages at all. The counts come off the spawn log instead of the message stream, which is the only record that survives that. reload_project reports them under ast_reload_health.parse_diagnostics, per category, with a capped location sample and the omitted count beside it. check turns the two soundness classes into AST_ASM_CLOBBER and AST_UNKNOWN_ATTRIBUTE, and folds every category nobody has classified into one AST_UNCLASSIFIED_WARNING entry keyed by category, because an entry per category grows with the program rather than with the finding. AST_WARNING_ALLOWLIST is the only way a category leaves that aggregate and starts empty: silence about a warning nobody has read would be this server calling it benign without saying so.

This comment was marked as resolved.

Sign in to view

jserv force-pushed the ast branch from b258dbc to f27f3ce Compare August 30, 2026 17:24