PaperlayerView exact revision on arXiv

Source-linked AI summary

AutoFraming: Synthesizing Dynamic Frames of C Code with LLMs

Han Zhou, Yu Luo, Dianxiang Xu

arXiv:2610.29046v1cs.AI

TL;DR

LLM-based C specification synthesis has paid limited attention to frame conditions, which describe modified memory, dependencies, and preserved state. AutoFraming analyzes CPGs to guide frame synthesis alongside functional contracts. It improves error-free frame results across two benchmarks and when added to existing synthesis tools.

  • Problem

    LLM-based ACSL synthesis has focused on functional specifications while giving little attention to frame conditions that specify affected memory, dependencies, and preserved state.

    Source: §I · p. 1

  • Method

    AutoFraming extracts frame-relevant information from CPGs, projects it into required frame obligations, and uses an LLM to complete and repair the surrounding ACSL contract.

    Source: §I · p. 1, E. Frame-constrained contract synthesis · p. 6

  • Results

    92.9% of 84 real-world functions receive error-free frames, a 179% relative improvement over the state-of-the-art baseline; performance also improves on the academic benchmark and in integrations.

    Source: §I · p. 1

  • Takeaways & Limitations

    CPG-grounded frame constraints yield more complete and reusable frame specifications than existing generators within the evaluated C and ACSL setting.

    Source: §VII · p. 11

    Error-free frame status reflects acceptance under the evaluated Frama-C/WP and dependency-analysis toolchain, not a complete semantic oracle; stronger-than-needed preconditions may exclude valid calls.

    Source: §VI · p. 10

Abstract

from arXiv · show

Large language models (LLMs) have shown considerable promise in synthesizing formal specifications from source code. However, existing approaches primarily focus on functional contracts and loop invariants, while largely neglecting frame conditions, which specify the memory locations that may or may not be modified during execution and constitute an essential part of formal specifications. To address this limitation, we propose an LLM-based approach for synthesizing ACSL frame specifications alongside functional contracts from C code. Our approach analyzes code property graphs (CPGs) to extract frame-relevant information from the input code and leverages this information to guide the LLM in generating accurate frame conditions. The resulting specifications capture both region-separation constraints and data dependencies that govern variable modifications. Experimental results demonstrate the effectiveness of our approach. On a benchmark of 84 ACSL-compliant functions from non-trivial real-world systems, our method successfully synthesizes error-free frame specifications for 92.9% of the functions, representing a 179% relative improvement over state-of-the-art techniques. On a second benchmark consisting of 51 functions, the success rate increases from 80.4% to 96.1%. Furthermore, when integrated as an auxiliary component into existing LLM-based ACSL-synthesis frameworks, our approach improves frame-specification generation performance by up to 61.9%.

I. INTRODUCTION

AutoFraming addresses the limited treatment of frame conditions in LLM-based ACSL synthesis by using CPG-derived information to guide frame generation. Its examples show why accurate frames require both memory separation and write dependencies, and the reported results show gains on two benchmarks and when integrated with existing tools.

I. INTRODUCTION

  • Existing LLM-based ACSL approaches emphasize functional specifications, while frame conditions describing affected memory, effect dependencies, and preserved memory receive little attention.Proof success alone may miss incomplete memory-dependence information or imprecise aliasing assumptions, leaving contracts too weak for modular reasoning.Source: §I · p. 1
  • AutoFraming analyzes CPG-derived memory interference, caller-visible writes, loop-indexed ranges, and dependencies, then uses a fixed frame skeleton to guide LLM contract generation and repair.Its frame analysis includes caller-visible roots, access windows, interfering pointer pairs, write-set locations, and dependence footprints; it can also augment Preguss and AutoSpec.Source: §I · pp. 1–2
  • 92.9% of 84 real-world functions receive error-free frames, a 179% relative improvement over the state-of-the-art baseline; on 51 academic functions, the rate rises from 80.4% to 96.1%.As an auxiliary component for existing tools, AutoFraming improves error-free frame performance by up to 61.9%.Source: §I · p. 1

II. A MOTIVATING EXAMPLE

  • A fully proved contract can still permit an invalid aliased call: writing through eaten may overwrite buf[1] before it is read, producing 6 rather than the intended 8.The example call satisfies the preconditions, but the pointers overlap; the function requires the relevant memory regions to be disjoint.Source: §II · p. 2
  • The desired dynamic frame specifies both disjointness between buf’s accessed region and eaten and that the value written to eaten depends on buf’s elements and len.The example’s ACSL contract expresses these as a \separated precondition and an assigns clause with a \from footprint.Source: §II · p. 3

A. Overview

AutoFraming uses a three-stage workflow to derive frame information from a CPG, project it into a frame skeleton, and have an LLM complete and repair the surrounding contract under verification feedback.

A. Overview

  • AutoFraming analyzes functions bottom-up, building a CPG for each function and extracting caller-visible roots, accessed regions, interfering pointer pairs, write locations, and dependencies.Bottom-up analysis makes verified callee contracts available when analyzing callers.Source: A. Overview · p. 3
  • The separation projection turns interfering pointer regions into disjointness requirements, while the dependence projection attaches caller-visible input footprints to write-set locations.The resulting frame obligations are treated as required constraints; candidates that delete or weaken them are rejected.Source: A. Overview · p. 3
  • The LLM assembles a verifier-checkable contract around the frame skeleton, and Frama-C feedback guides repair while preserving projected frame conditions and avoiding degenerate frames.Candidates are accepted only when they preserve the frame conditions and make proof progress.Source: A. Overview · p. 3

B. CPG-Based Frame Analysis

AutoFraming extracts five kinds of frame-relevant information from CPGs, combining syntax, control flow, and dependencies to recover memory regions, writes, and their influences.

B. CPG-Based Frame Analysis

  • AST, CFG, and PDG views contribute complementary evidence: syntax reveals write targets, control flow helps recover access ranges, and dependencies expose influences on writes.Together, these views determine caller-visible roots, access windows, interfering pointer pairs, write-set locations, and dependence footprints.Source: B. CPG-Based Frame Analysis · pp. 3–4
  • Caller-visible roots are formal parameters and globals that may be read or written; pointed-to types help filter pointer pairs that could overlap.Compatibility includes same-type, byte-level, generic-pointer, and cast-related accesses, while clearly incompatible types can be filtered when no such operations occur.Source: B. CPG-Based Frame Analysis · p. 4
  • Access windows record the entry-expressible regions a pointer may access, using CFG loop and guard information to recover constant offsets, loop ranges, and available bounds.These windows support separation constraints over accessed regions rather than pointer names alone.Source: B. CPG-Based Frame Analysis · p. 4
  • Interfering pointer pairs are those whose aliasing could affect a caller-visible write or its value; the test avoids separating unrelated pointer parameters.A root counts as affecting a write when it roots the write or is read into a value that flows to it.Source: B. CPG-Based Frame Analysis · p. 4
  • Write-set locations are caller-visible targets normalized for ACSL assigns clauses; loop-indexed array writes are expanded to ranges recovered from CFG loop and guard edges.Local pointer aliases may be used to rewrite a target to a caller-visible root, but are not emitted in the frame clause.Source: B. CPG-Based Frame Analysis · pp. 4–5
  • Each write location’s dependence footprint contains caller-visible inputs that influence its value through data or control flow, with local intermediates followed transitively.Pointer reads are lifted to accessed regions, so a loop writing from buf[i] contributes the accessed region of buf.Source: B. CPG-Based Frame Analysis · p. 5

C. Synthesis of Region-Separation Constraints

Region-separation synthesis must identify which caller-visible pointer regions require disjointness and determine their extents, despite aliasing and access patterns hidden in C code.

C. Synthesis of Region-Separation Constraints

  • A valid frame may require caller-visible regions to be disjoint because overlap can let a write through one pointer affect a read or write through another.The relevant regions may be hidden by pointer arithmetic, loop-indexed accesses, local aliases, casts, or library calls.Source: C. Synthesis of Region-Separation… · p. 5
  • AutoFraming identifies interfering pointer roots and their access windows, then projects each relevant pair into an explicit caller-side \separated precondition.It applies separation only when aliasing can affect the caller-visible frame, not merely because pointer types are compatible.Source: C. Synthesis of Region-Separation… · p. 5
  • Pointer roots and access windows are converted into entry-expressible memory regions, using constants, loop ranges, or available guard bounds to describe extents.When a window cannot be expressed at function entry, AutoFraming uses the strongest entry-expressible approximation and requires verification to preserve the frame obligations.Source: C. Synthesis of Region-Separation… · p. 5

D. Synthesis of Data Dependencies for Write Sets

AutoFraming attaches a dependence footprint to each write-set location, translating CPG-derived value-flow information into ACSL `\from` clauses. The resulting frame skeleton combines these clauses with region-separation preconditions.

D. Synthesis of Data Dependencies for Write Sets

  • For each location a function may modify, its frame must identify caller-visible inputs that can influence the written value.The final assignment alone may not reveal this dependence, which can flow through temporaries, aliases, loops, control predicates, globals, or library calls.Source: D. Synthesis of Data Dependencies for… · p. 5
  • AutoFraming uses each write-set location as a carrier for its CPG-extracted dependence footprint.The projection expresses internal value-flow information in the ACSL form used for modular verification.Source: D. Synthesis of Data Dependencies for… · p. 5
  • A dependence footprint includes control dependencies, so a flag can influence a written value even when absent from the assignment’s right-hand side.The `\from` clause must describe what the value depends on, not only where the function writes.Source: D. Synthesis of Data Dependencies for… · p. 6
  • The two projections form a frame skeleton with `\separated` preconditions and `assigns ... \from` clauses.When a location’s dependence footprint is empty, the projection emits an `assigns L \from \nothing` clause.Source: D. Synthesis of Data Dependencies for… · p. 6

E. Frame-constrained contract synthesis

AutoFraming places a projected frame skeleton into the contract as required obligations, while the LLM supplies the surrounding annotations needed for verification. This separates frame-critical analysis from verifier-facing contract completion.

E. Frame-constrained contract synthesis

  • The projected skeleton contains required `\separated` preconditions and `assigns ... \from` clauses that the LLM cannot invent or reinterpret.It is inserted into the prompt as required frame obligations.Source: E. Frame-constrained contract synthesis · p. 6
  • A complete contract may need validity preconditions, loop annotations, or auxiliary assertions to make the skeleton’s frame obligations provable.For example, a separated memory region must be well-formed and valid at function entry, and an assigned slice may require loop annotations.Source: E. Frame-constrained contract synthesis · p. 6
  • Access windows, write sets, and dependence footprints guide the LLM’s envelope with validity requirements, loop annotations, and relevant inputs for postconditions.For calls, a verified callee contract is supplied as context.Source: E. Frame-constrained contract synthesis · p. 6
  • Program analysis and projection produce the frame-critical skeleton, while the LLM supplies the verifier-facing envelope and functional context.This avoids relying on the LLM to guess dynamic-frame clauses from source code alone.Source: E. Frame-constrained contract synthesis · p. 6

F. Frame-constrained refinement

Frame-constrained refinement uses verifier feedback to repair incomplete surrounding annotations without weakening projected frame conditions. The evaluation is organized around synthesis performance, ablation, and generality.

F. Frame-constrained refinement

  • Refinement addresses failures caused by missing validity preconditions, loop annotations, or assertions needed to make projected frame conditions checkable.It uses feedback from Frama-C/WP and Eva.Source: F. Frame-constrained refinement · p. 6
  • The LLM may revise the contract, but projected frame clauses must remain and cannot be weakened or replaced by degenerate frames.Candidates with missing assigns clauses, missing loop assigns clauses, or vacuous frames that hide caller-visible writes are rejected.Source: F. Frame-constrained refinement · p. 6
  • A revision must close at least one unresolved proof obligation without reopening any already discharged obligation.Refinement ends when the relevant frame conditions are discharged or the maximum number of rounds is reached.Source: F. Frame-constrained refinement · p. 6

IV. EVALUATION

  • The evaluation asks how well AutoFraming synthesizes frame specifications, how its analysis and projection contribute, and whether it generalizes to existing frameworks.These are framed as performance, ablation, and generality questions.Source: §IV · p. 6

A. Datasets

The evaluation covers real-world and academic C functions and finds that AutoFraming substantially outperforms existing generators on frame-specific checks. Its remaining failures include verifier limits and cases where LLM generation changes the projected frame.

A. Datasets

  • Da contains 84 functions from nine real-world C programs; functions requiring user-defined inductive predicates are excluded.Db contains 51 Frama-C tutorial programs across eight categories.Source: A. Datasets · p. 7

B. Experimental Setup

  • A function counts as frame-error-free only if it passes assigns-warning, WP proof, and Eva dependency-set checks.Frame-condition timeouts count as failures; the study also reports the WP proof ratio.Source: B. Experimental Setup · p. 7

C. RQ1: How effectively does AutoFraming synthesize frame specifications?

  • The pipeline is tested with Gemini-2.5-Pro and GPT-5.2 against Preguss on both benchmarks and AutoSpec on Db.Verification uses Z3 and Alt-Ergo with a 30-second per-goal timeout.Source: C. RQ1: How effectively does… · p. 7, B. Experimental Setup · p. 7
  • Baseline weaknesses are mainly frame incompleteness: Preguss has 51 warnings on Da, while AutoFraming variants have two and four.On Db, each AutoFraming variant has one warning, compared with 10 for Preguss and 28 for AutoSpec.Source: C. RQ1: How effectively does… · p. 7
  • Some correct frames remain unverified when bounds depend on mutable runtime values, or when LLM generation overrides the projected frame.For example, the verifier cannot decide completeness for a range bounded by mutable m->num; in set_iv, an LLM's four-slice frame can time out where a contiguous range succeeds.Source: C. RQ1: How effectively does… · pp. 7–8
  • AutoFraming exceeds 90% frame-error-free success on both benchmarks, substantially outperforming existing generators.On Da, AF-Gemini reaches 92.9% (78/84) and AF-GPT 91.7% (77/84), versus Preguss at 33.3%; on Db, they reach 96.1% (49/51) and 94.1% (48/51), versus Preguss at 80.4% and AutoSpec at 45.1%.Source: C. RQ1: How effectively does… · pp. 7–8, Table II · p. 8, Table III · p. 8

D. RQ2: How do CPG-derived frame information and frame-

The ablation identifies frame-constrained projection as AutoFraming’s central component. Removing it sharply reduces frame-error-free results, while remaining failures arise mainly from dependence and write-set errors, with some region-separation failures.

D. RQ2: How do CPG-derived frame information and frame-

  • The three reduced variants remove CPG information, frame-constrained projection, or both, isolating their contributions alongside the full pipeline.The no-projection variant reaches 54 functions, close to the refinement-only variant’s 53; removing CPG information yields 48.Source: constrained projection contribute to… · pp. 8–9
  • Most remaining failures involve write-set data dependencies: omitted or unsound \from clauses, incorrect write extents, or missing modified locations.Examples include omitting an inner array dimension or failing to assign \result; some functions also have incorrect write sets such as \assigns \nothing despite writing outputs.Source: constrained projection contribute to… · p. 8
  • Other failures concern region separation, where weakened \separated preconditions prevent discharge of the frame condition despite a correct write set.Source: constrained projection contribute to… · p. 8
  • 78/84 functions are frame-error-free with the full pipeline, versus 54/84 without frame-constrained projection despite retaining CPG information and refinement.The 24-function drop indicates that CPG information alone does not replace translating it into ACSL frame clauses.Source: Table V · p. 9, constrained projection contribute to… · p. 9

E. RQ3: Can AutoFraming improve existing frameworks as a frame synthesis component?

As an auxiliary layer for existing ACSL generators, AutoFraming improves frame outcomes and verifier goal-prove rates. Earlier specification-inference approaches use traces, static analysis, or LLMs, but primarily target functional behavior and invariants rather than frame specifications.

E. RQ3: Can AutoFraming improve existing frameworks as a frame synthesis component?

  • AutoFraming augments Preguss and AutoSpec contracts by strengthening frame conditions rather than replacing the upstream generators.Source: E. RQ3: Can AutoFraming improve… · p. 9
  • AutoFraming increases verification goals while raising goal-prove rates: Preguss on Da goes from 1378 to 1687 goals and 94.0% to 96.8% proved.Added \separated preconditions and \from dependencies account for the added goals; on Db, AutoSpec’s goal-prove rate rises from 86.4% to 97.9%, and Preguss’s from 96.0% to 97.5%.Source: E. RQ3: Can AutoFraming improve… · p. 9
  • On Db, AutoSpec+AutoFraming reaches 50/51 frame-error-free functions (98.0%) versus 36/51 (70.6%) with AutoSpec+LLMRefine; Preguss+AutoFraming reaches 50/51 (98.0%) versus 39/51 (76.5%).Across integrations, frame-error-free rates rise to 95.2%–98.0%, while goal-prove rates and absolute proved goals also increase; the evaluated goal-prove rate does not establish semantic completeness of functional clauses.Source: E. RQ3: Can AutoFraming improve… · p. 9

A. Program-Analysis-Based Specification Inference

  • Program-analysis specification inference includes dynamic methods that mine execution traces and static methods that reason over program semantics.Trace-based methods can depend on input coverage and overfit observed executions; the surveyed approaches generally emphasize functional behavior rather than frame specifications.Source: A. Program-Analysis-Based… · pp. 9–10

B. LLM-Assisted Formal Specification Generation

Prior specification-generation research spans LLM-assisted C and ACSL tools and systems for other languages. The paper’s conclusion presents AutoFraming as a program-structure-guided approach, while identifying rule coverage, evaluation scope, and toolchain as boundaries.

B. LLM-Assisted Formal Specification Generation

  • For C, LLM-assisted specification systems use source-code prompts, analysis information, or verifier feedback, but mainly target functional contracts and loop invariants.Examples include AutoSpec’s iterative verifier-feedback refinement and Preguss’s decomposition of large verification tasks.Source: B. LLM-Assisted Formal Specification… · p. 10
  • LLM-assisted specification generation also targets Java, Rust, C++, and smart contracts, using approaches such as verifier repair, self-refinement, and execution validation.Source: B. LLM-Assisted Formal Specification… · p. 10

VI. THREATS TO VALIDITY

  • Uncommon C patterns, including complex pointer manipulation and unusual data dependencies, may escape the CPG-derived rules and leave specifications incomplete or verification goals unresolved.Benchmark overlap with LLM pretraining is also an internal-validity concern.Source: §VI · p. 10
  • Frama-C/WP acceptance and dependency diagnostics do not provide a complete semantic oracle; verified frames may impose unnecessarily strong preconditions that exclude valid calls.Goal-prove rate measures verifier discharge, not specification minimality or user intent.Source: §VI · p. 10
  • Evaluation covers 84 real-world C functions and 51 academic examples, and the approach is designed for ACSL with Frama-C/WP.Results may not generalize to all C programs, other languages or verification tools, or complex low-level features such as unrestricted casts and concurrency.Source: §VI · p. 10

VII. CONCLUSION

  • AutoFraming extracts frame information, projects it into a deterministic frame skeleton, and uses an LLM to complete and repair the surrounding contract with verifier feedback.The conclusion reports more complete and reusable frame specifications than existing generators and identifies richer heaps, recursive structures, library summaries, and additional languages and verifiers as future work.Source: §VII · pp. 10–11
Loading 2610.29046v1…