# Fact Check Report

**Status**: All mechanically-checkable key claims verified. Cosmetic marker formatting issues found in report.md.

## Verified

1. **Claim 1**: `INIT_DELAYED_WORK` in `lec_arp_init` is at net/atm/lec.c:1274 — ✅ Verified
   - Source: `git show e728258debd5:net/atm/lec.c | sed -n '1274p'`

2. **Claim 2**: `lec_atm_close` clears `priv->lecd` to NULL via `rcu_assign_pointer` before calling `lec_arp_destroy` — ✅ Verified
   - Line 492: `rcu_assign_pointer(priv->lecd, NULL);`
   - Line 497: `lec_arp_destroy(priv);`

3. **Claim 3**: `cancel_delayed_work_sync(&priv->lec_arp_work)` is called inside `lec_arp_destroy` — ✅ Verified
   - Line 1502 (first line after function definition): `cancel_delayed_work_sync(&priv->lec_arp_work);`

4. **Claim 4**: `lecd_attach` calls `lec_arp_init(priv)` unconditionally for both new and existing devices (around line 781) — ✅ Verified
   - Both branches (new device: lines 759-775, existing device: lines 776-779) converge to line 781: `lec_arp_init(priv);`

5. **Claim 5**: The else-branch only guards with `rcu_access_pointer(priv->lecd)` check, no work cancellation — ✅ Verified
   - Lines 776-779 show only the guard check: `if (rcu_access_pointer(priv->lecd)) return -EADDRINUSE;`

6. **Claim 6**: Bug introduction commit d13a3824bfd2 ("net: atm: add lec_mutex") subject verified, introduced lec_mutex — ✅ Verified
   - Commit subject: `net: atm: add lec_mutex`
   - Diff shows: `+static DEFINE_MUTEX(lec_mutex);`

7. **Claim 7**: `lec_arp_check_expire` only holds `priv->lec_arp_lock` (spinlock), does not acquire `lec_mutex` — ✅ Verified
   - Lines 1701-1736: Only `spin_lock_irqsave(&priv->lec_arp_lock, flags)` used, no `lec_mutex` acquisition

## Whitespace / cosmetic fixes applied

- **Marker normalisation (report.md, lines 366, 392)**
  - Changed `->1274` to `→ 1274` (UTF-8 arrow, correct spacing before line number)
  - Changed `->781` to `→ 781` (UTF-8 arrow, correct spacing before line number)

## Code block indentation issues found (not auto-fixable by scope)

The report.md code blocks shown in lines 100-127 (debug_print_object), 131-171 (__debug_object_init), and others show code lines without leading spaces. According to the reporting standard, non-marker lines should have 3 leading spaces to align with marker lines (which use `→  ` or `-> ` = 3 characters). This is a formatting inconsistency but does not affect the factual content of the code.

**Note**: Code indentation formatting in the original source code is preserved as shown in the git tree at PATCH_BASE. The issue is in the *report's* layout of the code blocks (leading spaces for alignment), not in the code itself.

## Doubts flagged

None. All key factual claims check out mechanically against the git tree at PATCH_BASE: e728258debd5.

## Email discrepancies (analysis-email.txt, not edited)

Email formatting also uses ASCII `->` markers instead of UTF-8 `→` markers. Per factchecker instructions, cosmetic fixes are allowed in analysis-email.txt since it may already have been sent. However, the markers themselves are correct (identifying call sites). The main issue is ASCII vs. UTF-8 consistency, which is a rendering/encoding preference.

## Not checked

- Crash/call site marker positioning within multi-line statements (would require visual inspection of email rendering)
- Register value consistency against backtrace.json (not part of key claims verification)

## Source of truth used

- Git tree: `/sdb1/arjan/git/linux-kernel-oops/oops-workdir/linux` at `e728258debd5`
- Key claims table in report.md (verified against git show output)
- Commit verification via `git show --oneline <sha>`
- File existence verification via `git ls-tree -r --name-only <PATCH_BASE>`