[Ada] Remove warnings-as-errors about constraints error in dead code

GNAT removes error messages attached to nodes within dead code; in particular, within instances of generic units with alternative branches for different generic formal types and parameters. Now this removal also works for error messages that come from warnings about constraint errors that have been

[Ada] Remove extra space in single object declarations

Fix whitespace in single object declarations; violations detected with a simple LKQL checker. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_aggr.adb, exp_attr.adb, exp_ch3.adb, exp_ch7.adb, exp_dist.adb, exp_util.adb, freeze.adb, frontend.adb, inline.ad

[Ada] Proof of System.Vectors.Boolean_Operations

This proves in SPARK the unit System.Vectors.Boolean_Operations. The specification models explicitly the array of Boolean represented by Vectors.Vector, so that the result of functions can be specified by expressing the relationship between input and output models. Tested on x86_64-pc-linux-gnu,

[Ada] Conformance error on protected subp with anonymous-access-to-tagged formal

The compiler incorrectly rejected a protected subprogram with a formal of an anonymous access type that designates a tagged type when the protected type extends an interface and the formal's designated type (a different type) is declared immediately within the same scope as the protected type; an e

[Ada] Tune inconsistent message about fixed-lower-bound and -gnatX

Use a dedicated routine to complain about the missing -gnatX switch. Previously the message was: error: fixed-lower-bound array is an extension feature; use -gnatX and after this change it is: error: fixed-lower-bound array is a GNAT specific extension error: unit must be compiled with -g

[Ada] Remove redundant initialization of Test_And_Set_Flag object

When expanding exception declarations we explicitly initialized the System.Atomic_Operations.Test_And_Set.Test_And_Set_Flag object with 0. This was redundant, because the Test_And_Set_Flag type has aspect Default_Value => 0. It is better to not duplicate this constant in the GNAT code, in case that

[Ada] Adapt ghost code to maintain proof

Add two assertions that are now required for the proof of System.Exp_Mod to go through. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-expmod.adb (Exp_Modular): Add assertions.diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb --- a/gcc/ada/l

[Ada] Proof of unit System.Case_Util

This unit is needed to prove System.Val_Bool, as it is used in System.Val_Util called from System.Val_Bool. Add contracts that reflect the implementation, as we don't want these units to depend on units under Ada.Characters. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * li

[Ada] Fix check for implicit allocation of dynamic objects

We check for dynamic objects by recursively examining record components. We should thus first check if the component is a record type before checking if it is a `Discriminated_Size` which will be false for all non array-type components. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/

[Ada] Reuse Make_Temporary where possible

Simplify: Make_Defining_Identifier (Loc, Chars => New_Internal_Name (C)); into: Make_Temporary (Loc, C); Code cleanup related to creation of itypes for allocators in GNATprove mode; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch7.adb

[Ada] Fix incomplete debug info for derived packed array type

The front-end was copying the Packed_Array_Impl_Type of the parent onto the derived type, which fools the logic of the debug back-end. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch3.adb (Analyze_Subtype_Declaration): In the case of an array copy Packed_Array

[Ada] Remove unnecessary block in code for expansion of allocators

Cleanup related to handling of allocators in GNATprove; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch4.adb (Size_In_Storage_Elements): Remove unnecessary DECLARE block; refill code and comments.diff --git a/gcc/ada/exp_ch4.adb b/gcc/

[Ada] PR ada/79724

Fix handling of e.g. gcc-11 in Osint.Program_Name. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ PR ada/79724 * osint.adb (Program_Name): Fix handling of suffixes.diff --git a/gcc/ada/osint.adb b/gcc/ada/osint.adb --- a/gcc/ada/osint.adb +++ b/gcc/ada/osint.adb @@ -2

[Ada] Recover proof of Ada.Strings.Fixed with assertions

Changes in GNATprove make it necessary to add assertions here. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-strfix.adb (Insert, Overwrite): Add assertions.diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb --- a/gcc/ada/libgnat/a-strfix.adb

[Ada] Deconstruct a VMS utility routine which is only used by GNATprove

Routine Compile_Time_Known_Value_Or_Aggr was needed for VMS compatibility, which was deconstructed in 2014. This routine was dead since then, until it got accidentally reused by GNATprove to pretty print counterexamples. Cleanup related to handling of compile-time-known null values in GNATprove.

[Ada] Adapt proof of System.Arith_Double

Following changes in GNATprove, ghost code needs some adjustments for proof to go through. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-aridou.adb (Double_Divide): Adjust proof of lemma Prove_Signs, call lemma for commutation of Big and multiplic

[Ada] Remove unreferenced name constants

In the Snames unit we had many unreferenced constants. Most of them are leftovers from features that have been deconstructed years ago, e.g. VAX support. Code cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * snames.ads-tmpl: Remove unreferen

[Ada] Balance parentheses in comments about allocators

Cleanup related to handling of allocators and compile-time-known null expressions in GNATprove. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch4.adb (Analyze_Allocator): Fix comment. * sem_eval.ads (Compile-Time Known Values): Likewise.diff --git a/gcc/ada/sem

[Ada] Reduce scope of declare block in analysis of allocators

Cleanup related to handling of allocators in GNATprove; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch4.adb (Analyze_Allocator): Move DECLARE block inside IF statement; refill code and comments.diff --git a/gcc/ada/sem_ch4.adb b/gcc/a

[Ada] Remove name constant used by GNATprove but not by GNAT

Revert recent removal of Name_Rpc, which is needed by GNATprove to detect calls to potentially blocking subprograms. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * snames.ads-tmpl: Restore Name_Rpc.diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl --- a/gcc/ada

[Ada] Avoid redundant checks for empty lists

Simplify "No (L) or else Is_Empty_List (L)" into "Is_Empty_List (L)", since Is_Empty_List can be called on No_List and returns True. Code cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch4.adb (Expand_N_Expression_With_Actions): Avoid

[Ada] Remove unreferenced CCG-specific routine Insert_Declaration

Routine Insert_Declaration was originally added for the Ada-to-C translator, because in C we can't have declarations within an expressions. However, it is no longer used, because now we insert declarations into N_Expression_With_Actions. Code cleanup related to inserting itypes in spec expressions

[Ada] Task arrays trigger spurious unreferenced warnings

Incremental patch to handle multi-dimensional arrays of tasks and records with task components. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.adb (Check_References): Add call to Has_Task instead of checking component type.diff --git a/gcc/ada/sem_warn.adb

[Ada] Accept square brackets for expression functions

Ada RM 6.8 allows an expression function to return an aggregate directly at the top level (enclosed with either parentheses or square brackets). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * par-ch6.adb (Scan_Body_Or_Expression_Function): Accept left bracket as tok

[Ada] Include generic instance names in non-visible entity errors

This patch adds the printing of generic instance names when encountering non-visible entities instead of just the line number of the package instantiation. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch8.adb (Nvis_Messages): Add generic instance name to error

[Ada] Relax assertion on designated types for equality operators

This will avoid doing artificial conversions during semantic analysis. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * gcc-interface/utils2.c (build_binary_op) : Relax a little the assertion on designated types of pointer types.diff --git a/gcc/ada/gcc-interface/util

<    30   31   32   33   34   35