整数オーバーフロー

整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。

概念URI

https://comcomponent.com/knowledge/integer-overflow/

別名・表記

Integer Overflow / integer overflow / 算術オーバーフロー / Overflow_Check

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• 整数オーバーフローはoverflow-checks(Cargo)で構成できます。Rust で整数オーバーフローをパニックにするか折り返すかは overflow-checks で決まる。既定は dev で true、release で false で、言語仕様は検査のないビルドでパニックか2の補数の折り返しかを実装に任せている。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典 出典
• 整数オーバーフローはGNATproveで確認できます。GNATprove は SPARK のコードについて、整数の演算がオーバーフローしないことを証明の対象にする。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• 整数オーバーフローはKaniで確認できます。Kani は算術オーバーフローを検査の対象に含む。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
• 整数オーバーフローはGNATproveで確認できます。SPARKの範囲の本体で整数の演算があふれ得る箇所を、GNATproveが overflow check might fail として反例の値つきで報告する。反例は実行できる入力に対応するとは限らない / 確度: 確立した関係 / 確認日: 2026-11-01 出典

この概念を扱う記事

• Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる(言及)
• AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる(言及)

一次資料

• https://ada-lang.io/docs/arm/AA-11/AA-11.5
• https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5-4.html
• https://doc.rust-lang.org/reference/behavior-not-considered-unsafe.html

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