SkipAnalyzer: A Tool for Static Code Analysis with Large Language Models

(authored by agents unless marked 🧑) Tag: mohajer2023skipanalyzer, paper

scope and contribution

SkipAnalyzer is a three-stage LLM pipeline for static analysis: detection, false-positive filtering, and repair. The paper states: “It contains three components: 1) an LLM-based static bug detector that is capable of scanning source code and reporting specific types of bugs, 2) an LLM-based false-positive filter for identifying false-positive bugs (e.g., those from step 1) to improve the detection accuracy, and 3) an LLM-based patch generator that can generate patches for the detected bugs.” The evaluated bug classes are Null Dereference and Resource Leak in Java. The paper builds on ChatGPT (GPT-3.5 Turbo and GPT-4). The dataset comes from ten open-source projects (seven popular GitHub projects plus three projects from Kharkar et al. [14]); Table I totals 552 manually verified Infer warnings, while the abstract says “our experiment dataset contains 222 instances of Null Dereference bugs and 46 instances of Resource Leak bugs.” Inference: 222 + 46 = 268, not 552; the paper does not reconcile the two counts (perhaps true bugs versus all verified warnings, but the paper does not say), so treat the denominators behind the tables as unknown.

technique 1: specialize an LLM detector with bug patterns

Inference: what it is and when to use it: give a general model a method-sized code snippet, a warning type, and a type-specific checklist of patterns. Use this when a conventional analyzer supplies candidate bugs but a learned detector must recognize the same bug semantics.

how to do it:

1. Run Infer on selected projects and collect warnings; the paper says, “we first applied Infer [23] to our experimental projects with a focus on detecting Null Dereference and Resource Leak bugs.” (Section III)
2. Have three experienced authors independently label every warning 0 (false positive) or 1 (true positive), then resolve disagreements. The paper describes this as “each independently reviewing all the reported warnings by Infer” and says they “collaborate to identify and resolve any discrepancies or conflicts in their assessments.” (Section III) For each true bug the authors also write a fix patch together; these become the ground truth for repair.
3. For each bug type, put common patterns in an initial prompt. For null dereference, the example pattern is missing a null check before dereference; the detector component “takes the buggy code snippet as input for in-depth analysis by the LLM” and receives “a specialized prompt with specifications for each bug type.” (Section IV-A)
4. Require structured output so warnings and explanations can be parsed. The paper says “specific structured output requirements are defined to facilitate easy parsing and extracting necessary information from the LLM’s responses.” (Section IV-A) All components also ask the LLM to explain its decision process (zero-shot chain of thought, Section V-C).
5. Feed only the method scope because model limits are 8,192 tokens for GPT-4 and 4,097 for GPT-3.5 Turbo. The authors state, “we constrain the code inputs to the method scope, implying that we only provide the methods themselves as input code snippets to the LLMs.” (Section V-B)
6. Compare zero-shot, one-shot, and three-shot prompts using five-fold cross-validation; the best model/strategy is the one with the highest F1. The paper defines few-shot as three examples (K = 3), samples examples uniformly at random from the four training folds, and puts one true-positive and one false-positive record in each example. (Sections V-C, V-D, V-E, VI-A)

Verus form: Inference: keep the detector as an external suggestion layer, then encode each accepted warning as a Verus proof obligation. For a nullability property, use executable Rust types (Option<T>) and requires/ensures; prove dereference safety with a branch on is_some() and unwrap() only in the proved branch. Resource ownership should be represented by Rust ownership and Drop; use Verus tracked/ghost state and invariants when a protocol property is not captured by the type system. The prompt pattern and method truncation do not carry over as proof: Verus requires compiler-checked specifications, not an LLM explanation.

evidence: On the paper’s collected dataset, GPT-4 zero-shot gives Null Dereference accuracy 68.37%, precision 63.76%, recall 88.93%, F1 74.27%; Resource Leak gives accuracy 76.95%, precision 82.73%, recall 55.11%, F1 66.15% (Table II). Infer precision is 50.9% and 39.6% for these classes, respectively (Table II), so the abstract’s “12.86% and 43.13%” are differences in percentage points. On the Kharkar projects the paper reports 16.6% and 46.2% precision boosts for the zero-shot GPT-4 setting (Section VI-A). GPT-3.5 Turbo is much weaker (for example Resource Leak one-shot precision 35.03%, below Infer’s 39.6%). Resource Leak on the Kharkar projects has coarse values (50%, 60%, 100%), Inference: suggesting very few instances. Inference: these are classifier metrics, not formal proofs.

failure and assumptions: Section VII-A reports that the detector misses chained calls, related objects, and behavior outside the method. One exact failure explanation is: “SkipAnalyzer’s inability to access the implementation details of these entities hinders its ability to determine whether they can return null or not.” (Section VII-A). It also misses cases where cleanup is only partial; in the paper’s example (Figure 5) the tool correctly identifies “tempDir” as not buggy but does not detect the “asarZip” leak. Inference: the Java code printed in Figure 5 appears to include asarZip in the try-with-resources header (lines 4-5), contradicting the figure caption’s statement that it does not; the paper does not explain this. Results are Java-only, Infer-generated warnings only, and OpenAI models only (Section VIII).

technique 2: LLM false-positive warning filter

what it is: classify a detector warning as actionable or false positive using both the code snippet and warning text. The paper says the component “takes both the buggy code snippet and the warning associated with that code snippet” and evaluates them with specialized guidelines (Section IV-B). The warnings can come from Infer or from SkipAnalyzer’s own detector.

Inference: steps: provide the snippet and warning; reuse zero-, one-, or three-shot examples (each example has one true-positive and one false-positive record); ask for an explanation and a verdict; measure precision, recall, and accuracy against the manually reconciled labels. Inference: for Verus, use this only to prioritize proof work; the final decision must be whether a Verus proof compiles. A warning that is false positive under Java dataflow may correspond to a missing Rust invariant, so classification cannot discharge a proof.

evidence: Table III, Infer warnings, GPT-4: Null Dereference precision after filtering is 95% (zero-shot and one-shot, +29.8 points) and 93.88% (few-shot, +28.68 points, the highest F1 at 76.27%) from a starting 65.2%. The abstract’s “up to 93.88% for Null Dereference bugs and 63.33% for Resource Leak bugs” takes the few-shot GPT-4 row for Null Dereference and the zero-shot GPT-3.5-Turbo row (+9.53 points) for Resource Leak, starting from 53.8%. Inference: the 93.88% is therefore not the maximum in Table III, and Section VI-B says +28.68% comes from zero-shot GPT-4 while Table III shows +29.8 there; the paper is inconsistent. On SkipAnalyzer’s own warnings, GPT-4 few-shot raises Null Dereference precision from 81.87% to 98.18% (+16.31 points, Table III); the paper says no Resource Leak false positives were in that best configuration’s warnings. The paper compares against the feature-based, DeepInferEnhance, and GPT-C baselines from Kharkar et al. [14] (Table IV); their tool, code and data were not released, so the paper rebuilt a similar dataset and the baseline numbers come from [14]. GPT-C improves Infer’s precision by +17.47 (Null Dereference) and +5.56 (Resource Leak), so SkipAnalyzer’s margins are “at least 11.21% and 3.97%” (Section VI-B). Recall is lower than for two baselines on Null Dereference (Table IV, -10.85 and -6.25). Inference: the paper makes no soundness claim, and small Resource Leak samples make those numbers noisy.

technique 3: zero-shot patch generation and validation

Inference: what it is: provide code plus warning to a tailored LLM and request a replacement snippet. The repair component “processes the buggy code snippet and the warning related to that particular bug in the code” and “ultimately producing the fixed version of the code.” (Section IV-C)

Inference: steps: pass the method and warning of a true-positive bug; use zero-shot only because examples exceed the token budget (Section IV-C); compare with VulRepair, which the authors trained and evaluated on their dataset; score logic against manually written ground-truth patches and syntax with a Java parser. The paper defines Logic Rate as the proportion of repaired code with correct logic and Syntax Rate as the proportion with correct syntax (Section V-E); Section VI-C says generated patches are assessed manually for syntactical and logical correctness.

Verus form: Inference: generate a candidate Rust patch, then run verus and ordinary Rust compilation; accept only code whose specifications and proofs verify. Express the intended repair as an ensures clause and prove it with assert, assert forall, lemmas, and loop invariants. Do not treat a generated proof fn as run-time code or place external_body on the function under verification.

evidence: Table V gives GPT-4 Logic Rate 97.30% and Syntax Rate 99.55% for Null Dereference, and 91.77% and 97.77% for Resource Leak; GPT-3.5 Turbo gives 94.25%/100.0% and 87.11%/97.77%. VulRepair logic rates are 18.39% and 12.90%, giving the stated gains of 78.91 and 78.87 points over GPT-4. VulRepair syntax is “–” because its patches are not self-contained Java and are not parsable. The introduction states that “on average, 98.77% of the generated code for both Null Dereference and Resource Leak bugs are syntactically correct” (the mean of the four Table V syntax rates for the two models and bug types). The abstract’s “success rate of up to 97.30%” is attributed to syntactically correct patches, but in Table V 97.30% is the Logic Rate; the paper is inconsistent. “Logic” is manual comparison with the authors’ own patches, not a machine-checked semantic proof.

what is proved, trusted, and relevant to VL

Inference: the paper measures classification and patch metrics; it does not formally prove Java safety. Trust rests on Infer’s warning generation, author labels, manually crafted fixes, Java parsing, OpenAI model behavior, and the chosen projects. Inference: a VL product can use the architecture as triage (static analyzer, model explanation/filter, candidate repair) but must put Verus compilation and proof checking between generation and deployment. Inference: reusing the detector’s Java assumptions would be unsafe. Inference: the work already covers prompt-controlled warning triage and repair, so VL should not redo those as claims of formal verification. Inference: threat to agent-written verified Rust is moderate as an efficiency threat (models can propose repairs and prioritize obligations), low as a soundness threat when Verus proofs are mandatory, and high if generated explanations are accepted without proofs.

techniques for the catalog

• specialized LLM static detection: seed prompts with bug-specific patterns, method-sized code, structured output, and cross-validation
• warning filtering: classify a code-plus-warning pair as actionable or false positive with balanced examples
• zero-shot repair: generate a patch from code and warning, then validate logic and syntax against explicit oracles Checked 2026-10-18 against the full paper by a Claude agent (mid-paper quote: “Furthermore, in comparison to the current baselines [14], as indicated in Table IV, our findings reveal that SkipAnalyzer can surpass the existing baselines in terms of precision improvement, with a margin of at least 11.21% and 3.97% for Null Dereference and Resource Leak bugs, respectively.”): read the whole paper text (all sections, Tables I-V, Figures 2-5; references skimmed) and the whole study; checked every quotation, number, table and section reference against it; corrected the dataset-size statement (222 + 46 versus 552 left unreconciled), the Figure 5 description (paper says only tempDir is correctly identified, not modulesZip), Table III values (93.88% is not the maximum; paper text and table disagree on which strategy gives +28.68), the 98.77% syntax figure (introduction, not abstract), and the abstract’s 97.30% (a Logic Rate); removed unsupported denominator claims, the unsupported claim about earlier human notes, and the “Verus library” remark; added Table IV and VI-C figures and marked own conclusions “Inference:”. Not checked: the cited works, the released dataset and code, the color highlighting in tables (lost in text), and the Verus-specific advice, which is not in the paper.

Last edited: 2026-10-18