Landing: c4edd89d9b52

← All landings

Project / Subsystem

gcc / ada

Date

2026-01-23

Author

Viljar Indus

Commit

c4edd89d9b52a651f66e11419b2d15c2652fc85b

Source

github

Perf win

Breaking

View on GitHub →

All attributes

project: gcc
subsystem: ada
patch_id: —
commit_hash: c4edd89d9b52a651f66e11419b2d15c2652fc85b
source_type: github
headline: Ada: Add missing assertion level check in SPARK mode.
tldr: The Ada compiler adds a missing check for assertion levels inside aspect specifications in SPARK mode.
author: Viljar Indus
outcome: committed
performance_win: false
breaking_change: false
series_id: —
series_parts: []
tags: • ada
• SPARK
• assertion
discussion_id_link: —
bugzilla_pr: —
url: https://github.com/gcc-mirror/gcc/commit/c4edd89d9b52a651f66e11419b2d15c2652fc85b
date: 2026-01-23T00:00:00.000Z

The Ada compiler adds a missing check for assertion levels inside aspect specifications, as described in rule 14 of SPARK RM 6.9. This enforces assertion levels within aspect specifications, ensuring compliance with the SPARK subset of Ada.