---
generated_at: 2026-02-17 21:30:00
metrics:
  claims_total: 146
  claims_with_evidence: 146
  claims_without_evidence: 0
confidence_derived: 1.00
---

# 根拠レポート：drnim モジュール単体テストケース一覧

## 本レポートについて

### 目的
本レポートは、生成された単体テストケース一覧の信頼性を検証し、人間レビュアーが効率的にレビューできるようにすることを目的としています。

### チェック方法
以下の観点でドキュメントの内容（Claim：主張）を検証しています：

1. **根拠の有無確認**：各主張に対して、ソースコード・既存設計書・要件定義書などの根拠（Evidence）が存在するか
2. **根拠との整合性**：主張の内容が根拠と矛盾していないか
3. **網羅性**：参照すべき情報源を適切にカバーしているか

### 信頼度スコアの算出
- **confidence_derived** = 根拠あり件数 / 総主張件数
- 状態「○」：根拠あり、「△」：根拠不足または要確認

### 本レポートの使い方
1. まず「サマリー」で全体の信頼度と優先レビュー項目を確認
2. 「Claims と根拠の対応」で △ の項目を重点的にレビュー
3. 「不足情報」で補完が必要な情報源を確認

---

## 1) サマリー（まず見るところ）
- 総合信頼度（derived）：**1.00**
  - 根拠あり：146 / 146、根拠なし：0
- 優先レビュー（高）
  1. **Z3連携処理のテストケース**：Z3ライブラリとの連携は外部依存があり、実際のテスト実行時に環境依存の問題が発生する可能性
  2. **エラーハンドリングのテストケース**：例外処理のテストは実行時の状態再現が困難な場合がある
  3. **コマンドライン処理のテストケース**：システム環境に依存するため、テスト環境の構築が必要

## 2) 参照した情報（Evidence一覧）
> ここに「実在するもの」だけ列挙。抽出フェーズで付けたIDをそのまま出す。

- E-01: `drnim/drnim.nim` - DrNimメインソースファイル（1272行）
- E-02: `drnim/tests/tphi.nim` - Phi関連テストファイル
- E-03: `drnim/tests/tbasic_array_index.nim` - 配列インデックステストファイル
- E-04: `drnim/tests/tensures.nim` - ensures/requiresテストファイル
- E-05: `drnim/tests/tsetlen_invalidates.nim` - setLen無効化テストファイル
- E-06: `docs/code-to-docs/単体テストケース一覧/plan.md` - プロジェクト計画書

## 3) Claims と根拠の対応（レビューの主戦場）

### isLoc関数（UT-DRN-001〜007）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-01 | nkSym(skLet)に対してtrueを返す | E-01 (L103-110) | ○ |
| C-02 | nkSym(skTemp)に対してtrueを返す | E-01 (L103-110) | ○ |
| C-03 | nkSym(skForVar)に対してtrueを返す | E-01 (L103-110) | ○ |
| C-04 | nkSym(skParam)でvar型でない場合にtrue | E-01 (L107-109) | ○ |
| C-05 | nkSym(skResult/skVar)でsfAddrTakenなしの場合 | E-01 (L133-134) | ○ |
| C-06 | nkDerefExprでassumeUniqueness=false時false | E-01 (L116-118) | ○ |
| C-07 | nkDerefExprでassumeUniqueness=true時継続処理 | E-01 (L116-118) | ○ |

### バージョン管理関数（UT-DRN-008〜014）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-08 | currentVarVersionが変数バージョンを返す | E-01 (L138-143) | ○ |
| C-09 | currentVarVersionでバージョン0の場合 | E-01 (L138-143) | ○ |
| C-10 | previousVarVersionが前バージョンを返す | E-01 (L145-150) | ○ |
| C-11 | previousVarVersionでバージョン未存在時 | E-01 (L145-150) | ○ |
| C-12 | disambがシンボルスコープIDを返す | E-01 (L152-158) | ○ |
| C-13 | 同名シンボル存在時のインクリメント | E-01 (L152-158) | ○ |
| C-14 | 新シンボルのmangler追加 | E-01 (L158) | ○ |

### stableName関数（UT-DRN-015〜021）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-15 | nkSymに対する安定名生成 | E-01 (L168-184) | ○ |
| C-16 | nkIntLitに対する数値文字列生成 | E-01 (L201-203) | ○ |
| C-17 | nkFloatLitに対する浮動小数点文字列 | E-01 (L204) | ○ |
| C-18 | nkStrLitに対するエスケープ文字列 | E-01 (L205-206) | ○ |
| C-19 | nkDotExprに対するドット区切り名 | E-01 (L207-210) | ○ |
| C-20 | nkBracketExprに対するブラケット形式 | E-01 (L211-215) | ○ |
| C-21 | isOld=true時の前バージョン名生成 | E-01 (L177-181) | ○ |

### notImplemented関数（UT-DRN-022〜024）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-22 | string引数でCannotMapToZ3Error | E-01 (L259-263) | ○ |
| C-23 | PNode引数でCannotMapToZ3Error | E-01 (L265-268) | ○ |
| C-24 | PType引数でCannotMapToZ3Error | E-01 (L270-273) | ○ |

### translateEnsures関数（UT-DRN-025〜026）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-25 | skResultシンボルの置換 | E-01 (L275-281) | ○ |
| C-26 | 非結果シンボルのコピー | E-01 (L278-281) | ○ |

### typeToZ3関数（UT-DRN-027〜031）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-27 | tyInt系のZ3_int_sort変換 | E-01 (L286-287) | ○ |
| C-28 | tyBoolのZ3_bool_sort変換 | E-01 (L288-289) | ○ |
| C-29 | tyFloat系のZ3_fpa_sort_double変換 | E-01 (L290-291) | ○ |
| C-30 | tyUInt系のZ3_bv_sort変換 | E-01 (L292-294) | ○ |
| C-31 | 未対応型のnotImplemented呼び出し | E-01 (L295-296) | ○ |

### nodeToZ3関数（UT-DRN-032〜054）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-32 | nkSymのZ3定数生成 | E-01 (L355-362) | ○ |
| C-33 | nkIntLitのZ3整数生成 | E-01 (L363-373) | ○ |
| C-34 | nkFloatLitのZ3浮動小数点生成 | E-01 (L374-375) | ○ |
| C-35 | mEqIのZ3_mk_eq生成 | E-01 (L380-382) | ○ |
| C-36 | mLeIのZ3_mk_le生成 | E-01 (L383-384) | ○ |
| C-37 | mLtIのZ3_mk_lt生成 | E-01 (L385-386) | ○ |
| C-38 | mAddIのZ3_mk_add生成 | E-01 (L406-407) | ○ |
| C-39 | mSubIのZ3_mk_sub生成 | E-01 (L408-409) | ○ |
| C-40 | mMulIのZ3_mk_mul生成 | E-01 (L410-411) | ○ |
| C-41 | mDivIのZ3_mk_div生成 | E-01 (L412-413) | ○ |
| C-42 | mModIのZ3_mk_mod生成 | E-01 (L414-415) | ○ |
| C-43 | mAndのZ3_mk_ite生成 | E-01 (L428-431) | ○ |
| C-44 | mOrのZ3_mk_ite生成 | E-01 (L432-434) | ○ |
| C-45 | mNotのZ3_mk_not生成 | E-01 (L437-438) | ○ |
| C-46 | mImpliesのZ3_mk_implies生成 | E-01 (L439-440) | ○ |
| C-47 | mForallのforallToZ3呼び出し | E-01 (L443-444) | ○ |
| C-48 | mExistsのexistsToZ3呼び出し | E-01 (L445-446) | ○ |
| C-49 | mMaxIのZ3_mk_ite生成 | E-01 (L416-419) | ○ |
| C-50 | mMinIのZ3_mk_ite生成 | E-01 (L420-423) | ○ |
| C-51 | mOldの旧バージョンZ3定数生成 | E-01 (L474-483) | ○ |
| C-52 | mLengthSeqのZ3整数定数生成 | E-01 (L387-398) | ○ |
| C-53 | mHighの(len-1)式変換 | E-01 (L399-403) | ○ |
| C-54 | mLowのlowBound変換 | E-01 (L404-405) | ○ |

### addRangeInfo関数（UT-DRN-055〜058）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-55 | 整数型シンボルの範囲情報追加 | E-01 (L553-555) | ○ |
| C-56 | tyRange型の明示的範囲情報追加 | E-01 (L542-544) | ○ |
| C-57 | tyFloat系は範囲情報なし | E-01 (L545-547) | ○ |
| C-58 | len関数呼び出しの0以上範囲情報 | E-01 (L559-571) | ○ |

### Z3ユーティリティ関数（UT-DRN-059〜065）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-59 | on_errのZ3Exception送出 | E-01 (L589-592) | ○ |
| C-60 | forallの変数リスト付きZ3式生成 | E-01 (L594-601) | ○ |
| C-61 | forallの変数リスト空時implies式 | E-01 (L600-601) | ○ |
| C-62 | conjのZ3_mk_and生成 | E-01 (L603-607) | ○ |
| C-63 | conjの空条件時Z3_mk_true | E-01 (L606-607) | ○ |
| C-64 | setupZ3のZ3コンテキスト初期化 | E-01 (L609-616) | ○ |
| C-65 | setupZ3のエラーハンドラ設定 | E-01 (L616) | ○ |

### 証明エンジン関数（UT-DRN-066〜076）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-66 | proofEngineAuxの証明成功時 | E-01 (L618-676) | ○ |
| C-67 | proofEngineAuxの証明失敗時 | E-01 (L668-673) | ○ |
| C-68 | proofEngineAuxのValueError時 | E-01 (L674-676) | ○ |
| C-69 | proofEngineのDrCon初期化 | E-01 (L678-685) | ○ |
| C-70 | skipAddrのnkHiddenAddr処理 | E-01 (L687-688) | ○ |
| C-71 | skipAddrの非HiddenAddr処理 | E-01 (L687-688) | ○ |
| C-72 | translateReqのskParam変換 | E-01 (L690-699) | ○ |
| C-73 | translateReqの引数不足エラー | E-01 (L694-695) | ○ |
| C-74 | translateReqの非パラメータコピー | E-01 (L696-699) | ○ |
| C-75 | requirementsCheckのrequires検証 | E-01 (L701-708) | ○ |
| C-76 | requirementsCheckのValueError時 | E-01 (L706-708) | ○ |

### compatibleProps関数（UT-DRN-077〜079）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-77 | 互換proc型でtrue | E-01 (L710-762) | ○ |
| C-78 | 非互換proc型でfalse | E-01 (L710-762) | ○ |
| C-79 | effect情報なし時true | E-01 (L758-762) | ○ |

### ファクト管理関数（UT-DRN-080〜085）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-80 | addFactのfacts追加 | E-01 (L766-770) | ○ |
| C-81 | addFactの論理式分解 | E-01 (L768-769) | ○ |
| C-82 | negの否定ノード生成 | E-01 (L772-775) | ○ |
| C-83 | addFactNegの否定ファクト追加 | E-01 (L777-778) | ○ |
| C-84 | combineFactsのand結合 | E-01 (L780-784) | ○ |
| C-85 | combineFactsの片方nil時 | E-01 (L781-782) | ○ |

### prove関数（UT-DRN-086〜087）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-86 | prove成功時true | E-01 (L786-790) | ○ |
| C-87 | prove失敗時false+警告 | E-01 (L788-789) | ○ |

### traversePragmaStmt関数（UT-DRN-088〜090）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-88 | wAssumeプラグマ処理 | E-01 (L792-802) | ○ |
| C-89 | wAssertプラグマ処理 | E-01 (L798-802) | ○ |
| C-90 | wInvariantプラグマ処理 | E-01 (L798-802) | ○ |

### requiresCheck関数（UT-DRN-091〜092）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-91 | requires検証実行 | E-01 (L804-813) | ○ |
| C-92 | 検証失敗時警告 | E-01 (L812-813) | ○ |

### freshVersion関数（UT-DRN-093〜094）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-93 | 変数バージョン追加 | E-01 (L815-819) | ○ |
| C-94 | ルート変数なし時処理なし | E-01 (L816-817) | ○ |

### collectEnsuredFacts関数（UT-DRN-095〜096）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-95 | ensures効果の収集 | E-01 (L835-844) | ○ |
| C-96 | tyVar引数のfreshVersion呼び出し | E-01 (L837-839) | ○ |

### checkLe/checkBounds/checkRange関数（UT-DRN-097〜101）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-97 | checkLeの整数比較検証 | E-01 (L846-856) | ○ |
| C-98 | checkLeの浮動小数点比較 | E-01 (L849-850) | ○ |
| C-99 | checkBoundsの配列境界検証 | E-01 (L858-860) | ○ |
| C-100 | checkRangeのtyRange検証 | E-01 (L862-870) | ○ |
| C-101 | checkRangeの非tyRange処理 | E-01 (L863-864) | ○ |

### addAsgnFact関数（UT-DRN-102）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-102 | 代入ファクト追加 | E-01 (L872-877) | ○ |

### traverse関数（UT-DRN-103〜110）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-103 | nkReturnStmtのensuresCheck | E-01 (L1053-1056) | ○ |
| C-104 | nkCallKindsのrequiresCheck | E-01 (L1057-1063) | ○ |
| C-105 | nkAsgnのtraverseAsgn | E-01 (L1090) | ○ |
| C-106 | nkIfStmtのtraverseIf | E-01 (L1110) | ○ |
| C-107 | nkWhileStmtの条件付きファクト追加 | E-01 (L1112-1121) | ○ |
| C-108 | nkForStmtの範囲ファクト追加 | E-01 (L1122-1151) | ○ |
| C-109 | nkBracketExprの境界チェック | E-01 (L1168-1172) | ○ |
| C-110 | nkConvの範囲チェック | E-01 (L1158-1162) | ○ |

### traverseIf関数（UT-DRN-111〜112）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-111 | 各分岐のファクト追加と走査 | E-01 (L904-991) | ○ |
| C-112 | 分岐後のPhi情報構築 | E-01 (L992-1007) | ○ |

### traverseAsgn関数（UT-DRN-113〜114）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-113 | 代入時のfreshVersion呼び出し | E-01 (L1040) | ○ |
| C-114 | old参照付き代入ファクト | E-01 (L1041) | ○ |

### traverseCase/traverseTryStmt関数（UT-DRN-115〜118）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-115 | case分岐の走査 | E-01 (L888-894) | ○ |
| C-116 | case後のファクト復元 | E-01 (L894) | ○ |
| C-117 | try文の走査 | E-01 (L881-886) | ○ |
| C-118 | try後のファクト復元 | E-01 (L886) | ○ |

### disableVarVersions/varOfVersion関数（UT-DRN-119〜120）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-119 | 変数バージョン無効化 | E-01 (L896-898) | ○ |
| C-120 | バージョン付き変数参照生成 | E-01 (L900-902) | ○ |

### strongSemCheck関数（UT-DRN-121〜122）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-121 | Z3初期化と走査実行 | E-01 (L1176-1190) | ○ |
| C-122 | Z3リソース解放 | E-01 (L1189-1190) | ○ |

### mainCommand関数（UT-DRN-123〜125）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-123 | コールバック登録 | E-01 (L1197-1198) | ○ |
| C-124 | nimDrNimシンボル定義 | E-01 (L1202) | ○ |
| C-125 | コンパイル実行 | E-01 (L1204-1206) | ○ |

### processCmdLine関数（UT-DRN-126〜128）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-126 | コマンドライン解析 | E-01 (L1210-1244) | ○ |
| C-127 | --assumeUniqueオプション処理 | E-01 (L1233-1234) | ○ |
| C-128 | 引数エラー報告 | E-01 (L1241-1244) | ○ |

### handleCmdLine関数（UT-DRN-129〜131）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-129 | optStaticBoundsCheck有効化 | E-01 (L1247) | ○ |
| C-130 | 引数なし時ヘルプ表示 | E-01 (L1253-1255) | ○ |
| C-131 | メインコマンド実行 | E-01 (L1257-1260) | ○ |

### その他ユーティリティ関数（UT-DRN-132〜146）
| Claim ID | 主張 | Evidence | 状態 |
|---|---|---|---|
| C-132 | getCommandLineDescのヘルプ生成 | E-01 (L55-58) | ○ |
| C-133 | helpOnErrorのヘルプ表示と終了 | E-01 (L60-62) | ○ |
| C-134 | echoFactsのデバッグ出力 | E-01 (L93-97) | ○ |
| C-135 | paramNameのskParam名生成 | E-01 (L345-349) | ○ |
| C-136 | paramNameのskResult名生成 | E-01 (L348) | ○ |
| C-137 | paramNameのその他シンボル名 | E-01 (L349) | ○ |
| C-138 | forallToZ3の全称量化子変換 | E-01 (L342) | ○ |
| C-139 | existsToZ3の存在量化子変換 | E-01 (L343) | ○ |
| C-140 | nodeToDomainの'..'演算子処理 | E-01 (L308-309) | ○ |
| C-141 | nodeToDomainの'..<'演算子処理 | E-01 (L310-312) | ○ |
| C-142 | nodeToDomainの未知演算子エラー | E-01 (L313-314) | ○ |
| C-143 | ensuresCheckのensures検証 | E-01 (L1018-1024) | ○ |
| C-144 | ensuresCheckの条件なし時処理なし | E-01 (L1019-1023) | ○ |
| C-145 | translateEnsuresFromCallのmOld変換 | E-01 (L821-826) | ○ |
| C-146 | translateEnsuresFromCallのskParam変換 | E-01 (L827-830) | ○ |

## 4) 不足情報（Unknown / Missing）
- なし
  - 全てのテストケースは `drnim/drnim.nim` のソースコードに基づいて生成されており、根拠が明確です

## 5) リスクフラグ（レビュー観点）
- **0: 低リスク** - 全テストケースがソースコードの実装に基づいており、根拠が明確

### 注意点
1. **Z3ライブラリ依存**: DrNimはZ3 SMTソルバーに依存しているため、テスト実行にはZ3のインストールが必要
2. **コンパイラ内部構造依存**: テスト対象がNimコンパイラの内部データ構造（PNode, PSym, PType等）に依存しているため、コンパイラバージョンの変更により影響を受ける可能性
3. **静的リンク**: UNIXシステムではZ3が静的リンクされるため、ビルド環境の構築が必要

## 6) レビュアーチェックリスト（最小）
- [ ] Z3連携処理（UT-DRN-027〜065）のテストケースが実行環境で動作可能か確認
- [ ] 証明エンジン（UT-DRN-066〜076）のテストケースが網羅的にカバーしているか確認
- [ ] コマンドライン処理（UT-DRN-126〜131）のテストケースが全オプションをカバーしているか確認
- [ ] traverse系関数（UT-DRN-103〜118）のテストケースが全ノード種別をカバーしているか確認
- [ ] 既存のテストファイル（E-02〜E-05）との整合性を確認
