[CSA] Clang Static Analyzer Report - 130 findings

[github-actions[bot]]

Clang Static Analyzer Report

Date: 2026-02-25
Commit: 5ccc2cd - recompile
Build type: Debug (CMake + Ninja)
Analyzer: scan-build-18 (LLVM 18.1.3)

---

Summary

Metric	Count
Total findings	130
High severity (core.CallAndMessage)	80
Null dereference (core.NullDereference)	15
Dead code (deadcode.DeadStores)	27
Bitwise shift overflow (core.BitwiseShift)	15
Divide by zero (core.DivideZero)	5
Uninitialized values (core.uninitialized.*)	12
Other issues	6
Files affected	84

---

Changes Since Last Run

Comparison with 2026-02-24 (commit c282ece):

• Total findings: 130 (unchanged from 130)
• Status: No change in total count
• The findings remain consistent with the previous analysis

---

High-Priority Findings

Critical: Null Pointer Dereferences and Calls (95 findings)

These are the most serious findings that could lead to crashes or undefined behavior:

Top Issues by File:

1. src/ast/ast.h - Multiple null pointer calls (~18 instances)

   • Lines: 947, 1399, 1400, 1401 - Called C++ object pointer is null

2. src/ast/sls/sls_seq_plugin.cpp - 6 instances

   • Repeated null pointer dereferences in sequence plugin logic

3. src/math/realclosure/realclosure.cpp - 5 instances

   • Line 1118: Array access results in null pointer dereference
   • Lines 3461, 3477, 3494: Called C++ object pointer is null
   • Line 4109: Dead store (sign variable)

4. src/ast/euf/euf_mam.cpp - 5 instances

   • Lines 1167, 1405, 2160: Called C++ object pointer is null
   • Line 1708: Access to field 'm_opcode' results in null pointer dereference

5. src/math/polynomial/polynomial.cpp - 3 instances

   • Line 2581: Access to field 'm_next' results in null pointer dereference (m_del_eh)
   • Line 2587: Access to field 'm_next' results in null pointer dereference (m_next)

---

Findings by Category

Core Checkers (Memory Safety & Logic Errors)

1. core.CallAndMessage (80 findings)

Calls to C++ member functions through null object pointers. These are false positives in many cases due to analyzer limitations with complex invariants, but some may be real issues.

Notable locations:

• src/ast/ast.h (18 instances)
• src/smt/smt_context.h (7 instances)
• src/ast/sls/sls_seq_plugin.cpp (6 instances)
• src/util/util.h (5 instances)

2. core.NullDereference (15 findings)

Direct dereferences of null pointers through array access or pointer operations.

Examples:

• src/util/debug.cpp:163 - Intentional null dereference for crash testing
• src/math/realclosure/realclosure.cpp:1118 - Array access with null pointer
• src/ast/rewriter/enum2bv_rewriter.cpp:92, 100 - Args array access

3. core.BitwiseShift (15 findings)

Bitwise shift operations that overflow or use negative shift amounts.

Affected files:

• src/util/bit_util.cpp - 4 instances (shifts by 32 on unsigned int)
• src/math/simplex/bit_matrix.cpp - 5 instances (shifts by 32-35 on int)
• src/util/mpff.cpp - 2 instances (negative right operand)
• src/ast/rewriter/enum2bv_rewriter.cpp:67 - Left shift overflow

Status: Some are intentional (checked elsewhere), others may need review.

4. core.DivideZero (5 findings)

Potential division by zero operations.

5. core.uninitialized.* (12 findings)

• core.uninitialized.UndefReturn - Returning null references
• core.uninitialized.Branch - Branching on uninitialized values
• core.uninitialized.ArraySubscript - Array access with uninitialized index

6. core.StackAddressEscape (1 finding)

• src/qe/mbp/mbp_arrays.cpp:533 - Stack address escapes in model evaluator

---

Dead Code and Logic Errors

deadcode.DeadStores (27 findings)

Values stored to variables that are never read. These are typically harmless but indicate potential logic errors or unnecessary code.

Top occurrences:

• src/util/util.cpp:79, 108 - Variable 'v' stores never read
• src/math/hilbert/hilbert_basis.cpp:1013, 1014 - 'prod' and 'non_zeros'
• src/math/simplex/model_based_opt.cpp:76 - 'sign' variable
• src/bv_rewriter.cpp:2169 - 'bv_size' variable
• Various other locations across math and AST modules

---

Undefined Behavior

core.UndefinedBinaryOperatorResult (4 findings)

Operations with garbage/uninitialized values:

• src/ast/act_cache.cpp:178, 179, 200 - Bitwise AND with garbage values

---

Top Affected Files

File	Warnings	Primary Issues
src/ast/ast.h	18	Called null object pointer
src/smt/smt_context.h	7	Called null object pointer
src/ast/sls/sls_seq_plugin.cpp	6	Null dereferences, null calls
src/util/util.h	5	Called null object pointer
src/math/simplex/bit_matrix.cpp	5	Bitwise shift overflow
src/math/realclosure/realclosure.cpp	5	Null dereferences, dead stores
src/ast/euf/euf_mam.cpp	5	Null dereferences, null calls
src/smt/mam.cpp	4	Called null object pointer
src/util/bit_util.cpp	4	Bitwise shift overflow
src/math/lp/nla_core.cpp	4	Various issues

---

Build Log Excerpt

Sample warnings from build (click to expand)

[5/885] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o
/home/runner/work/z3/z3/src/util/debug.cpp:163:16: warning: Dereference of null pointer [core.NullDereference]

[6/885] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.o
/home/runner/work/z3/z3/src/util/bit_util.cpp:222:41: warning: Right shift by '32' overflows [core.BitwiseShift]
/home/runner/work/z3/z3/src/util/bit_util.cpp:286:37: warning: Left shift overflows [core.BitwiseShift]

[77/885] Building CXX object src/math/realclosure/CMakeFiles/realclosure.dir/realclosure.cpp.o
/home/runner/work/z3/z3/src/math/realclosure/realclosure.cpp:1118:30: warning: Array access results in null pointer dereference [core.NullDereference]
/home/runner/work/z3/z3/src/math/realclosure/realclosure.cpp:3461:37: warning: Called C++ object pointer is null [core.CallAndMessage]

[301/885] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal.cpp.o
/home/runner/work/z3/z3/src/util/parray.h:155:29: warning: Array access results in null pointer dereference [core.NullDereference]

[311/885] Building CXX object src/sat/CMakeFiles/sat.dir/sat_aig_finder.cpp.o
/home/runner/work/z3/z3/src/sat/sat_aig_finder.cpp:198:27: warning: Dereference of null pointer (use_list) [core.NullDereference]

scan-build: Analysis run complete.
scan-build: 130 bugs found.

---

Notes

• This report was generated automatically by the Z3 CSA Analysis workflow
• Many findings may be false positives: The analyzer has limited understanding of Z3's invariants (e.g., assertions, preconditions)
• Known intentional patterns: Some findings like debug.cpp:163 are intentional (crash test code)
• Human review recommended: Before acting on any finding, review the HTML report for full context
• Reproducibility: To reproduce locally, run:

  mkdir build && cd build
  scan-build-18 cmake -DCMAKE_BUILD_TYPE=Debug -G Ninja ../
  scan-build-18 -o /tmp/csa-report ninja

---

HTML Report

Full interactive HTML report with detailed execution paths: /tmp/csa-report/2026-02-25-090950-373-1/index.html

To view the complete report with execution traces for each finding, run:

scan-view /tmp/csa-report/2026-02-25-090950-373-1

---

Recommendations

1. Prioritize: Focus on core.NullDereference and core.DivideZero findings first
2. Review bitwise shifts: Check if the overflow patterns in bit_util.cpp and bit_matrix.cpp are intentional
3. Clean up dead stores: Remove unused variable assignments in math modules
4. Add assertions: For complex invariants that the analyzer can't infer, add runtime assertions
5. Consider suppressions: For known false positives, add inline comments explaining why the code is safe

---

_{Report generated by Z3 CSA Workflow on 2026-02-25}

AI generated by Clang Static Analyzer (CSA) Report

• expires on Mar 4, 2026, 10:39 AM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-04T10:39:14.004Z.

Closed by Workflow