Landing: b0483f456043

← All landings

Project / Subsystem

gcc / ada

Date

2026-03-13

Author

Javier Miranda

Commit

b0483f45604396756a0131f724ed4464d45c68dd

Source

github

Perf win

Breaking

View on GitHub →

All attributes

project: gcc
subsystem: ada
patch_id: —
commit_hash: b0483f45604396756a0131f724ed4464d45c68dd
source_type: github
headline: Ada: Implement missing overflow check for Integer_128 in GNATProve mode
tldr: Adds overflow checks for universal integer to 128-bit integer conversions in GNATProve to enhance code verification.
author: Javier Miranda
outcome: committed
performance_win: false
breaking_change: false
series_id: —
series_parts: []
tags: • ada
• gnatprove
• overflow
• verification
discussion_id_link: —
bugzilla_pr: —
url: https://github.com/gcc-mirror/gcc/commit/b0483f45604396756a0131f724ed4464d45c68dd
date: 2026-03-13T00:00:00.000Z

Under GNATProve mode, the Ada frontend previously lacked overflow checks for type conversions of universal integer numbers to 128-bit integer types. This commit adds the missing checks, ensuring that conversions are safe and within the valid range of the target type. This enhancement improves the reliability of code verified with GNATProve.