pragma Annotate(GNATprove)

GNATproveの検査メッセージを、理由を添えて誤検知(False_Positive)または意図したもの(Intentional)として正当化するプラグマ。直前の項目に掛かり、正当化した理由は解析結果の記録に残る。

概念URI

https://comcomponent.com/knowledge/spark-pragma-annotate/

別名・表記

検査メッセージの正当化 / False_Positive / Intentional

上位概念

SPARK

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• GNATproveはpragma Annotate(GNATprove)を利用します。GNATproveはpragma Annotateで正当化された検査メッセージを、失敗ではなく正当化済みとして扱い、理由を解析結果の記録に残す / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• コードレビュー(プルリクエストレビュー)はpragma Annotate(GNATprove)に対する本記事の推奨です。検査メッセージの正当化はすべてレビューする。誤った正当化は、実際に失敗し得る検査を隠す / 確度: 確立した関係 / 確認日: 2026-11-01 出典

この概念を扱う記事

• AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる(言及)

一次資料

• https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_use_gnatprove_in_a_team.html

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。