Claire Dross
1079ac32ac
Update legality rules for Iterable
2026-02-06 10:13:15 +00:00
Claire Dross
3f15907d9c
Add additional rules for overlays in the RM
...
Those rules are already enforced by the tool.
2026-02-05 15:21:54 +00:00
Claire Dross
ecf292a4bc
Fix LRM to say that P'Access is supported
2026-02-05 15:21:07 +00:00
Claire Dross
ca9557a334
Describe move to constants in the LRM
...
They are already handled in the tool.
2026-02-05 15:20:30 +00:00
Claire Dross
311ca923bc
Say that immutable discriminants cannot have relaxed initialization
2026-02-05 15:19:44 +00:00
Claire Dross
f17cd26a1d
Add rules to disallow UC on types with access subcomponents
...
Add an assumption for the allowed case and make the warning guaranteed.
2026-02-05 10:56:29 +00:00
Claire Dross
feefcbc3e5
Remove rule about Program_Exit on ghost subprograms
2026-02-05 10:55:17 +00:00
Claire Dross
76f0ac8e9c
Disallow dispatching calls on types with untagged partial view
2026-02-04 14:58:42 +00:00
Johannes Kanig
945faa2603
Remove last references to SPARK Discovery
2026-02-04 08:59:57 +00:00
Claire Dross
05b3f7469c
Allow ghost entity in aspects that apply to dependent ghost entities
...
It is now possible to mention a ghost entity E in an aspect of an
entity that depends on E. For pragmas occuring inside ghost entities
it was already allowed.
2026-01-22 14:31:39 +00:00
Martin Clochard
4641f50fbc
Document that exceptions shall not escape finally section in SPARK
2026-01-21 15:29:17 +00:00
Claire Dross
8fb7ee4b16
Accept assertion level in the grammar of Abstract_State
2026-01-06 15:22:53 +00:00
Claire Dross
1018c9fd77
Document functional trees in the UG
2025-12-04 14:24:05 +00:00
Piotr Trojanek
01c95a1abb
Objects with Async_Writers must be explicitly initialized
...
We agreed that it is safer for volatile variables (or state abstractions) with
Async_Writers to be explicitly initialized (or imported), despite SPARK RM
7.1.2(14) didn't require them to be initialized.
[changelog]
* docs/lrm/source/packages.rst
(External State): Remove rule 7.1.2(14); renumber subsequent rules.
* src/flow/flow-control_flow_graph-utility.adb
(Make_Variable_Attribute): Remove implementation of the mentioned rule.
* testsuite/gnatprove/tests/932__flow_async_import/test.out
New check on a volatile variable with no explicit initialization.
2025-12-02 12:54:14 +01:00
Johannes Kanig
8212f1a8bb
Fix documentation for pragma Compile_Time_Error
2025-11-28 00:04:00 +00:00
Johannes Kanig
f72794657d
Remove mention of body mode from UG
2025-11-10 00:46:59 +00:00
Andres Toom
03cadbda63
Minor whitespace fix
2025-10-28 15:14:44 +02:00
Claire Dross
0786727123
Apply 12 suggestion(s) to 1 file(s)
...
Co-authored-by: Tony Aiello <aiello@adacore.com >
2025-10-28 08:30:28 +00:00
Claire Dross
5f062c9510
Document restriction on predefined equality on accesses in the UG
2025-10-28 08:30:28 +00:00
Johannes Kanig
da4d09c3db
Remove sources for Japanese UG
2025-10-24 10:33:45 +09:00
Martin Clochard
9e0ec1bf8c
Reject ghost subprograms with Exit_Cases mentioning Program_Exit
2025-10-22 09:52:00 +00:00
Johannes Kanig
eed66e3ca6
Cleanup after removing SPARK discovery
2025-10-21 07:30:09 +00:00
Claire Dross
993050f6ec
Adapt the documentation on precisely supported address clauses
...
To take into account the case of slices which need aliased components
to be precisely supported.
2025-10-21 07:26:49 +00:00
Johannes Kanig
1466b5d504
Document that we depend on compiler assumptions
2025-10-20 08:57:18 +00:00
Anthony Leonardo Gracio
22d6ed84e9
Remove mention of Project Properties in SPARK UG
...
Mention the editing capabilities (completion, tooltips etc) provided
by GNAT Studio on project files instead.
For eng/ide/gnatstudio#569
2025-10-20 07:56:36 +00:00
