[Ada] Proof of System.Generic_Array_Operations at silver level

Proof of the generic unit to array operations (vector/matrix), only at silver level, for runtime errors that come from the generic part of the unit. This does not prove e.g. absence of overflows in an instantiation related to arithmetic operations passed as formal generic subprogram parameters. Ju

[Ada] Remove unnecessary declare block

Code cleanup related to handling of warnings-as-errors. Semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * errout.adb (Adjust_Name_Case): Remove unnecessary declare block.diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb --- a/gcc/ada/errout.

[Ada] Warn on subtype declaration of null range

This patch adds a warning on a subtype declaration with a compile-time-known range constraint that is a null range. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_res.adb (Resolve_Range): Warn on null range, unless we are inside a generic unit or an instance the

[Ada] Small cleanup of osint-m.adb

We remove the "pragma Elaborate_All (Osint)", because it is no longer needed. That allows us to remove the "with Osint" (i.e. with of our own parent). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * osint-m.adb: Remove with_clause and pragma.diff --git a/gcc/ada/osint-m.adb

[Ada] Warn on import of parent package

There is no need to say "with P;" in package P.Q. This patch adds a warning for that case. We also remove with clauses in our own code that trigger the warning. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch10.adb (Check_Redundant_Withs): Add a warning if a

[Ada] Add an option to Get_Fullest_View to not recurse

This option is used by GNAT LLVM. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.ads, sem_util.adb (Get_Fullest_View): Add option to not recurse and return the next-most-fullest view.diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem

[Ada] treepr: Print value of static expression

When printing a node, if it happens to be an integer-like expression whose value is known, print that value. This makes debugging a little easier. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * treepr.adb (Print_Node_Ref): Print the value if available.diff --git a/gcc/ada/t

[Ada] Use non-internal representation for access subprograms if UC to Address

If we have an Unchecked_Conversion between an access to subprogram and System.Address, we want to try to use a thin subprogram pointer. Try to do this automatically as much as possible and add one to the RTS. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/g-spipat.a

[Ada] treepr: print value only for discrete types

Follow-on to previous change "Print value of static expression". Print only if the type is discrete. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * treepr.adb (Print_Node_Ref): Change "not Is_Array_Type" to "Is_Discrete_Type".diff --git a/gcc/ada/treepr.adb b/gcc/ad

[Ada] Check scalar range in arrays constructed by concatenation

When concatenating scalars, we should check their range as in the following example: type uint8 is range 0 .. 255; type Array_Type is array (Positive range <>) of uint8; Array_1 : Array_Type := 42 & 256; This commit leads to emitting: - a warning if a constraint error is expected but

[Ada] Remove unnecessary guards for appending non-empty lists

Calls to Append_List and Append_List_To applied with empty lists do nothing, so there is no need to explicitly guard against such calls. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch3.adb (Build_Init_Procedure): Remove unnecessary guard. * exp_disp.adb (Make

[Ada] Remove unnecessary guard for inserting non-empty list

Calls to Insert_List_After and Insert_List_Before applied to empty lists do nothing, so there is no need to explicitly guard against such calls. Code cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch3.adb (Expand_N_Object_Declaration):

[Ada] Consistent suppression for warnings inside null loops

Warnings for nodes inside null loops were suppressed if posted with Error_Msg_NLE and emitted if posted with other error-reporting routines. This was inconsistent and error-prone. Part of removing quotes around exception names in messages, because messages without quotes will be now emitted by Err

[Ada] Fix inconsistent quoting in messages about compile-time errors

In some messages of the form "XXX_Error will be raised at run time" the XXX_Error was enclosed in quotes, in other it was not. Now all messages of this form are emitted without quotes. Note: in messages emitted from routine Possible_Local_Raise we still quote names of exceptions, but there indeed

[Ada] Fix comment about subprogram unnesting and unconstrained arrays

The original code for subprogram unnesting used 'Access for unconstrained arrays. This was recently changed to 'Unchecked_Access for GNAT-to-LLVM, but a reference to 'Access still appears in the comment. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_unst.adb (Unnest_Su

[Ada] Update -gnatwr doc for import of parent package

This construct is now flagged with -gnatwr. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_ugn/building_executable_programs_with_gnat.rst: Update -gnatwr documentation. * gnat_ugn.texi: Regenerate.diff --git a/gcc/ada/doc/gnat_ugn/building_executabl

[Ada] Remove explicit expansion of block with general case statement

When a general case statements is rewritten into a block, it is enough to call Analyze on this block node, because analysis of non-expressions automatically triggers expansion. Cleanup originating from investigating many variants of routines for (pre)analysis and resolution. Tested on x86_64-pc-l

[Ada] Fix exit status of GNAT.Expect.Close call on running process

Fix exit status processing logic in __gnat_waitpid. Fix GNAT.Expect.Interrupt on Windows. It was terminating the calling process. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * expect.c (__gnat_waitpid): Use macros WIFEXITED, WEXITSTATUS, WIFSIGNALED, WTERMSIG, WI

[Ada] Remove extra space before THEN keywords

Style cleanup; semantics is unaffected. Offending occurrences found with: $ grep "[A-Za-z0-9\)]+ +then$" -C 3 and reviewed manually, because some of them were due to explicit layout. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch5.adb, exp_disp.adb, exp_util.ad

[Ada] Simplify traversal in hooking of transient scopes

Subprogram calls can be detected with just Traverse_Func, we don't need a separate global variable or a Traverse_Proc (which is a wrapper for Traverse_Func with a yet another variable). Cleanup related to handling of transient scopes in various routines for (pre)analysis and resolution. Semantics

[Ada] Remove repeated routines for printing AST in Mixed_Case

Code cleanup; behaviour is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * osint.adb (To_Lower): Clarify that only To_Lower function causes bootstrap issues; fix style. * treepr.adb (Print_Str_Mixed_Case): Reuse existing case conversion ro

[Ada] Fix a couple of issues with pragma Inspection_Point

The first issue is that the pragma may require the address of the objects subject to it to have their address taken, like Asm_Input and Asm_Output, so these objects need to be specifically marked. The second issue is that the detection of unfrozen objects was not robust enough and would miss objec

[Ada] Fix __gnat_kill on Windows

Terminate process only on terminating signals. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * adaint.c (__gnat_kill): Terminate process only in case of SIGKILL, SIGINT, SIGBREAK, SIGTERM, SIGABRT. Do not call OpenProcess if not going to terminate process.di

[Ada] Spurious error caused by order of interfaces in full view

The frontend reports a spurious error when the order of interfaces differ between the full view and the partial view of a private type defined in a generic unit. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch3.adb (Reorder_Interfaces): When the conflicting in

[Ada] Cleanup and modification of unreferenced warnings

This patch modifies the behavior of pragma Unreferenced to be consistent in its behavior, by counting all variables specified as "Out" actual parameters as being referenced instead of only the first "Out" parameter. Additionally, much related duplicated has been removed. Tested on x86_64-pc-linux-

[Ada] More default initialization for multi-dim array aggregates

Expansion of multi-dimensional array aggregates with boxes (e.g. "(others => (others => <>))" only applied default initialization to components of a scalar type with Default_Value aspect and of an access type (which are initialized by default to null). Now default initialization is applied to comp

[Ada] Crash in class-wide pre/postconditions

The compiler may crash processing a class-wide pre/postcondition that has dispatching calls using the Object.Operation notation. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * atree.ads (Traverse_Func_With_Parent): New generic subprogram. (Traverse_Proc_With_Parent)

[Ada] Fix style in expansion of multi-dimensional array aggregates

Cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_aggr.adb (Build_Array_Aggr_Code): Fix inconsistent style in comments and code.diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_a

[Ada] Fix layout of pragma Inline in generated AST unit

Make the generated nmake.ads unit look more like it was written with GNAT style rules in mind; semantics is unaffected. Cleanup related to fix of default initialization in multi-dimensional arrays, which used to explicitly call the Nmake.Make_Null routine. Tested on x86_64-pc-linux-gnu, committed

[Ada] Fix uses of pragma Unreferenced in MinGW runtime unit

GNAT now emits more warnings about pragma Unreferenced. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnarl/s-taprop__mingw.adb (Timed_Sleep): Remove "pragma Unreferenced" for Result. (Timed_Delay): Likewise.diff --git a/gcc/ada/libgnarl/s-taprop__mingw.

[Ada] Fix the check of the 'Old prefix

The check did miss the part of Ada 2022 RM 6.1.1 (27/5) that the use of an entity declared within the postcondition expression is allowed if it's declared within the prefix itself. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_attr.adb (Check_Reference): Fix condition.

[Ada] Read directory in Ada.Directories.Start_Search rather than Get_Next_Entry

The Ada.Directories directory search function is changed so the contents of the directory is now read in Start_Search instead of in Get_Next_Entry. Start_Search now stores the result of the directory search in the search object, with Get_Next_Entry returning results from the search object. This di

[Ada] Task arrays trigger spurious unreferenced warnings

This patch fixes an issue in the compiler whereby objects of task arrays would trigger spurious unreferenced warnings. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.adb (Check_References): Handle arrays of tasks similar to task objects.diff --git a/gcc/ada

[Ada] Fix error on too large size clause for bit-packed array

The compiler should give again a warning instead of an error, which comes from an improper Esize set on the bit-packed array type by Layout_Type. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_pakd.adb (Install_PAT): Do not reset the alignment here. * layout.adb

[Ada] Switch from __sync to __atomic builtins for atomic counters

Unit System.Atomic_Counters was using deprecated __sync GCC builtins. Now it uses __atomic builtins, which are recommended for new code. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-atocou__builtin.adb (Decrement, Increment): Switch from __sync to __atom

[Ada] Adjust the alignment to the size for bit-packed arrays

This fixes a fallout of the latest change, which removed a problematic line resetting the alignment of the PAT type. It turns out that the alignment must now be adjusted for modular PAT types, as done in other contexts, to be consistent with the size. Tested on x86_64-pc-linux-gnu, committed on t

[Ada] Disable expansion of pragma Loop_Variant in CodePeer mode

Pragma Loop_Variant is expanded into code which is too complicated for CodePeer to handle and results in messages with internal names. Disable expansion. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_prag.adb (Expand_Pragma_Loop_Variant): Disable expansion in C

[Ada] Remove CodePeer annotations for pragma Loop_Variant

Pragma Loop_Variant is now expanded into a null statement in CodePeer mode. Remove annotations related to false positives in runtime units. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-exponn.adb, libgnat/s-expont.adb, libgnat/s-exponu.adb, libgnat/s-wid

[Ada] Switch from __sync to __atomic builtins for Lock_Free_Try_Write

Routine Lock_Free_Try_Write was using deprecated __sync GCC builtins. Now it uses __atomic builtins, which are recommended for new code. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-atopri.ads (Atomic_Compare_Exchange): Replaces deprecated Sync_Compare_A

[Ada] Make pragma Inspection_Point work for constants

This entails marking the pragma as requiring an lvalue and explicitly going to the corresponding variable of the constants, which is always built since the front-end marks the constants as having their address taken. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * gcc-interf

[Ada] Fix internal error on unchecked union with component clauses

The issue arises when the unchecked union contains nested variants, i.e. variants containing themselves a variant part, and is subject to a full representation clause covering all the components in all the variants, when the component clauses do not align the variant boundaries with byte boundaries

[Ada] Fix bogus error on call to subprogram with incomplete profile

This fixes a bad interaction between the machinery used to build subprogram types referencing incomplete types and the Copy-In/Copy-Out mechanism used to implement In/Out and Out parameters of elementary types in subprograms. The latter mechanism cannot be finalized until after incomplete types ar

[Ada] Use atomic builtins for atomic counters on x86 (32bit)

Remove the x86-specific (32bit) variant of System.Atomic_Counters, because the __atomic builtins work fine on all x86 CPUs except for i386, where they can be provided by libatomic (when compiling with -march=i386). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * Makefile.rtl

[Ada] Document LLVM-specific flags

Add documentation for new -gnatd_u and old -gnatd_R flags used for GNAT LLVM and its CCG. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * debug.adb: Add documentation for new -gnatd_u and old -gnatd_R flags used for GNAT LLVM and its CCG.diff --git a/gcc/ada/debug.ad

[Ada] Escalate pre-continuation messages from warnings to errors

When a compile-time constraint error is inserted into the AST, we emit a main message (e.g. "value not in range of ...") and its continuation (e.g. "Constraint_Error will be raised at run time"). When the main message is emitted as a warning and the continuation is escalated into an error, the main

[Ada] Code cleanups

Use membership tests when possible Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch9.adb, gen_il-types.ads, make.adb, par-ch12.adb, sem_ch13.adb: Use membership tests.diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada

[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

<    4   5   6   7   8   9