[Ada] Syntax error on "not null procedure"

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
Give an error in the following cases: type T is access not null procedure ...; type T is access not null function ...; type T is access not null protected procedure ...; type T is access not null protected function ...; These are illegal syntax. Note that similar errors on access-to-o

[Ada] Fix crash on pragma Compile_Time_Warning/Error

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
This patch fixes a compiler crash that occurs in the following situation: The file being compiled with's a generic package. The body of that generic package contains a procedure that does not have a separate spec (i.e. the procedure body acts as the spec). The procedure body instantiates another ge

[Ada] Do not return freeze nodes for start of early call regions

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
This makes sure that the Early Call Region Processor in Sem_Elab does not return a region starting with a construct that is not suitable for being included into it, for example a freeze node. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_elab.adb (Previous_Suitable_Con

[Ada] Allow formal functions to have a default in the form of an expression function

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
As a language extension, the declaration of a generic formal function is allowed to have a default given by an expression in parentheses, where the expression is of the function's result type and can refer to formal parameters of the function (in direct analogy with expression functions). For exam

[Ada] Tune whitespace of the bounded lists Aggregate aspect

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
Whitespace cleanup only. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-cbdlli.ads (List): Remove extra space in Aggregate aspect.diff --git a/gcc/ada/libgnat/a-cbdlli.ads b/gcc/ada/libgnat/a-cbdlli.ads --- a/gcc/ada/libgnat/a-cbdlli.ads +++ b/gcc/ada/libg

[Ada] Fix incorrect fixed-point computation in expression function

2021-12-01 Thread Pierre-Marie de Rodat via Gcc-patches
This fixes a couple of issues pertaining to (ordinary) fixed-point types declared with a Small aspect whose value is not equal to the default one. The processing of this aspect is delayed until the freeze point of the type, which means that the Small_Value of the entity for the type does not have

[Ada] Fix possible memory corruption for hostnames longer than 1024 bytes

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
When a hostname has more than 1024 characters, Constraint_Error is raised if the runtime is compiled with checks on, otherwise a memory corruption occurs. Use the constant NI_MAXHOST to ensure that the appropriate buffer size is allocated for the hostnames. Tested on x86_64-pc-linux-gnu, committed

[Ada] More intuitive names in sanity-checking of derived types

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Routine Check_Derived_Type used generic names for local variables, e.g. Elmt, List, Subp. This patch renames them to be more intuitive, in particular, using Derived_ and Parent_ prefixes for variables related to derived and parent types, respectively. Cleanup related to expansion of dispatching eq

[Ada] Proof of Boolean'Image and Boolean'Value

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This proves the functionality of the runtime support for these attributes that print and parse a Boolean value. As a side-effect of this proof, fix a possible range check failure in System.Val_Bool.Value_Boolean and a possible overflow check failure in System.Val_Util.Normalize_String. GNATprove

[Ada] Proof of System.Val_Util utilities for 'Value support

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This proves the functionality of the utility procedures supporting the implementation of 'Value attributes. As a side-effect of this proof, fix possible range check failures. GNATprove is run with switch --level=3. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-

[Ada] Add contract to Ada.Task_Identification.Activation_Is_Complete

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Description of Activation_Is_Complete was amended in AI12-0231-1. This routine raises a Program_Error when called with Null_Task_Id. Add an explicit contract to make GNATprove aware of the restriction. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnarl/a-taside.ads (Ac

[Ada] Proof of Interfaces.C with SPARK

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This proves the functionality of Interfaces.C with GNATprove. Ada RM specifications are added as comments in the spec, next to the formalization of specifications as contracts. As a side-effect of this proof, fix two errors in the 4 procedure versions of To_Ada, which may raise a range check fail

[Ada] vx7r2cert/light-tasking-rtp: undefined refs on ppc/ppc64

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Vx7r2cert ppc/ppc64 targets use the gcc toolchain, which requires a slightly different forumulation of libraries for the rts-light-tasking-rtp runtime. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * vxworks7-cert-rtp-link__ppcXX.spec: New file. * Makefile.rtl: Use i

[Ada] Remove duplicated condition in warnings about read-before-write

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Code for warnings about read-before-write of a variable had one condition in the outer IF statement and then the very same condition in an inner IF statement. Cleanup related to spurious warning on 'Initialized. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.adb (

[Ada] Simplify iteration over record components

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Iterate over record components with First_Component/Next_Component and not with First_Entity/Next_Entity. Change in Sem_Warn unit is related to spurious warning on 'Initialized; other occurrences of the same pattern were found with grep. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/

[Ada] Don't allow entry in implicit with chain to be ghost

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
When we add an entry to the implicit with chain of a unit while adding an RTS unit, we must not mark it as a ignored ghost statement because it points to the next with in the chain. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * rtsfind.adb (Maybe_Add_With): Ensure that the

[Ada] Refactor nested loops in warning on unassigned out parameter

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
For warning about unassigned out parameter we had a loop over all formal parameters which contained another loop over all formal parameters. This was inefficient. Cleanup related to spurious warnings about 'Initialized. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_wa

[Ada] Split spec and body of expression function with Subprogram_Variant

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Due to a latent bug with freezing, the expression function with Subprogram_Variant which was recently added to the System.Val_Util unit triggers a crash in CodePeer. Ordinary compilation was not affected by this bug, because of the Assertion_Policy (Ghost => Ignore) applied to this unit. Tested o

[Ada] Separate building of equality from other dispatching routines

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
For GNAT we create dispatching equality together with other dispatching routines (e.g. for stream reading and writing). For GNATprove we need to create only the dispatching equality. This patch separates it, so that it can be created from a SPARK-specific expansion. Tested on x86_64-pc-linux-gnu,

[Ada] Enable expansion of dispatching equality for GNATprove

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
For GNAT the dispatching equality is generated in expansion of freezing nodes. For GNATprove this expansion needs to be specifically enabled and must occur in a carefully setup context. Previously type freezing for GNATprove only involved building of the DIC procedure, which didn't require much co

[Ada] Inline all calls in Ada.Task_Identification

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Code cleanup; all routines in Ada.Task_Identification had pragma Inline except Activation_Is_Complete (and Image, which should rather stay like that). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnarl/a-taside.ads (Activation_Is_Complete): Add pragma Inline.di

[Ada] Enhance freezing code for instantiations

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This makes it possible for the freezing code to let the back-end establish a proper order of elaboration of package and subprogram instantiations in more cases, in particular with circularities, by placing freeze nodes for them later in the expanded code in these cases. Tested on x86_64-pc-linux-g

[Ada] Remove extra space after assignment symbol

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Fix style issues in GNAT after spotting a similar problem in one of the tests for GNATprove. These are easy to find with grep, but still require a manual inspection, because we want to preserve layout in declaration lists like: A := 1; B := 10; C := 100; Tested on x86_64-pc-linux-gnu, co

[Ada] Cleanups related to expansion of dispatching primitives

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Assorted cleanups related to expansion of dispatching primitives on derived types for GNATprove; semantics of the compiler is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/standard_and_implementation_defined_restrictions.rst (No_Dispatching_

[Ada] Use bracket aggregates in Ada2022

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Make bracket syntax array and container aggregates available with -gnat2022. Parenthesis syntax is not accepted anymore for container aggregate but can still be used for array aggregates. The latter is considered obsolete and a warning is emitted with -gnatwj. The warning is also temporarily disab

[Ada] Cleanup insertion of single freezing actions

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Replace calls to Ensure_Freeze_Node & Append_Freeze_Actions (plural) with a simple call to Append_Freeze_Action (singular), which calls Ensure_Freeze_Node itself. Cleanup related to expansion of dispatching primitives for GNATprove; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committe

[Ada] Cleanup detection of suspension objects

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Current implementation of Is_Suspension_Object is a leftover from an old code of Is_Descendant_Of_Suspension_Object, which used RTE_Available and indeed couldn't be called from GNATprove. Now Is_Descendant_Of_Suspension_Object can work with Is_RTE, which can be safely called from GNATprove. Clean

[Ada] Add pragma Annotate for CodePeer analysis

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
CodePeer issues a spurious message on the analysis of the loop variant in s-widthi.adb. Similarly to the same for s-widthu.adb, add a pragma Annotate to justify this message. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-widthi.adb: Add pragma Annotate.diff --git

[Ada] Proof of support units for 'Width on signed integers

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This replicates the proofs performed for 'Width on modular integers to the units that support 'Width on signed integers. Also add a minimal postcondition to the System.Width_U. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-widint.ads: Mark in SPARK. * lib

[Ada] Amend proof of System.Arith_Double to remove justifications

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
The proof of System.Arith_Double contained 11 occurrences of pragma Annotate to justify unproved checks, 10 of which for calls to Raise_Error denoting a case where the input leads to a division by zero or an overflow, and one for a loop invariant regarding an assumption on Single_Size. That should

[Ada] Reset internal flags for -gnatD and -gnatG

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This resets the internal flags associated with the -gnatD and -gnatG switches once the generated code is printed, so that it does not end up being printed twice in case something goes wrong after this point. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sprint.adb (Source_

[Ada] Fix obsolete array aggregate warning being triggered by expanded code

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
Filter out nodes not coming from source before emitting the warning. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_aggr.adb (Resolve_Array_Aggregate): Filter out nodes not coming from source before emitting the warning.diff --git a/gcc/ada/sem_aggr.adb b/gcc/ad

[Ada] Invalid memory access on finalization of class-wide type

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This patch is the first part of a correction for issues in the compiler whereby finalization of a heap-allocated class-wide type may cause an invalid memory read at runtime when the type in question contains a component whose type has alignment specified. Tested on x86_64-pc-linux-gnu, committed o

[Ada] Proof of System.Arith_32 for double arithmetic on 32bits

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This replicates in a simpler setting the proofs performed for generic unit System.Arith_Double. Note that it makes a difference to declare functions Big as expression functions here instead of renamings, as some checks are not proved with renamings, so expression functions are used instead. GNATp

[Ada] Fix packing for array component with discriminated part

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This restores the packing for a record type that contains a component of an array type whose component type is a record type with a subcomponent that is of a discriminated record type with variable size. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * gcc-interface/gigi.h (a

[Ada] Do not back-annotate maximum size for limited types

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This prevents gigi from back-annotating a maximum size for the Esize of limited record and concurrent types, in keeping with the implementation of Analyze_Object_Declaration for objects of these types. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * gcc-interface/decl.c (gna

[Ada] Remove obsolete a-assert

2021-12-02 Thread Pierre-Marie de Rodat via Gcc-patches
This package is a leftover after the change for using the base compiler's runtime during bootstrap. It is not used anymore. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * gcc-interface/a-assert.ads, gcc-interface/a-assert.adb: Remove.diff --git a/gcc/ada/gcc-interface/a-ass

[Ada] Revert r12-6599 (Fix up handling of ghost units [PR104027])

2022-04-27 Thread Pierre-Marie de Rodat via Gcc-patches
That change was short-circuiting too much, the regular processing (in particular writing ALI files) was bypassed, causing troubles with e.g. gnatmake or gprbuild down the road. Thanks to r12-6943, this is no longer necessary, so revert it. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada

[Ada] Stabilize exit code on close process

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Call Kill before close input handler in Close routine. Otherwise close input handler can terminate process before Kill and exit code became unpredictable. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/g-expect.adb (Close): Call Kill before Close_Input.diff --git a

[Ada] Remove doubly-negated tests for empty lists

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Replace "not Is_Non_Empty_List (...)" with "Is_Empty_List (...)". Code cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch5.adb (Update_Choice_Index): Simplify condition. * sem_ch8.adb (Attribute_Renaming): Likewise.diff --git a/

[Ada] Remove unused parameter from __gnat_kill

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Remove close parameter from __gnat_kill because it is not used in implementation. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * adaint.c (__gnat_kill): Remove close parameter. (__gnat_killprocesstree): Do not provide close parameter on call to __gnat_kill.

[Ada] Revamp type resolution for comparison and equality operators

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The main goal was to make it symmetrical, but this also moves error handling entirely to the second phase of type resolution. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * einfo.ads (Access Kinds): Reorder and beef up. * sem.adb (Analyze): Call Analyze_Comparison_E

[Ada] Remove redundant call to Set_Etype for attribute Bit_Order

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Node created by a call to New_Occurrence_Of (RTE (...), ...) has its Etype set. There is no need to follow it with a call to Set_Etype. Cleanup of various Analyze/Resolve routines. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_attr.adb (Analyze_Attribute): Don't call

[Ada] Remove repeated analysis of attribute prefixes

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
At the beginning of Analyze_Attribute routine we analyze the attribute prefix. There is no need to repeat this analysis in branches for individual attributes. Code cleanup related to various Analyze/Resolve routines. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_attr.

[Ada] vx21.07: stack-checking on ppc

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
On VxWorks >= 7.2 and 653, signal processing code is expected to clear the TCB exception count field when returning control back to user code. This change arranges to do so. It is believed that this is only an issue in Kernel mode, and not RTP because there is no exception count field in RTP mode

[Ada] Add utility to preanalyze assert expression without forcing its type

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
In SPARK loop and subprogram variants we now allow expressions of any discrete type or of Ada.Numerics.Big_Numbers.Big_Integers.Big_Integer type. This requires a variant of Preanalyze_Assert_Expression that doesn't force the expression to be of a particular type, similar to the existing variant of

[Ada] Allow Big_Integer in loop and subprogram variants

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
In SPARK loop and subprogram variants we now allow expressions of any discrete type and of Ada.Numerics.Big_Numbers.Big_Integers.Big_Integer type. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_prag.adb (Expand_Pragma_Loop_Variant, Expand_Pragma_Subprogram_Varia

[Ada] Use "aspect" instead of "pragma" in warnings

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
For warnings related to the Unreferenced, Unmodified, and Unused aspects, refer to the "aspect", not the "pragma". Note that the aspect can be set by an aspect_specification or a pragma, so the term "aspect" is correct even in the pragma case. However, messages in sem_prag.adb use Fix_Error, so th

[Ada] Refine description of SPARK with static Boolean expressions

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
A number of SPARK pragmas controlled by an optional Boolean expression require those expressions to be static. This is now clarified in the GNAT RM. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_pragmas.rst (Abstract_State, Async_

[Ada] Fix check for looking for user defined literals

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Recall that Has_Possible_Literal_Aspects only comes in if a given node does not have any visible interpretation. If one operand is a literal we assume that there may be a user-defined literal defined for some type to be determined during the downward pass of resolution, but that depends on the exis

[Ada] Fix visibility inside declare_expression

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The first implementation just created a scope for the analysis of the declarations and the expression, so that visibility would just work as it does for all other constructs. However this led to an annoying bug when one of the declarations or the expression itself creates a transient scope: there m

[Ada] Fix internal error on declaration of derived discriminated record type

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
When the parent type has a variant part and the derived type is also discriminated but statically selects a variant, the initialization routine of the derived type may attempt to access components of other variants that are no longer present. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/

[Ada] Properly handle unprefixed references to components

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
In some cases, the compiler would incorrectly reject unprefixed uses of component names in an aspect specification for the composite type. Correct this error. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch13.adb (Replace_Type_Ref): In the case of an identifier

[Ada] Fix package installation for private array type of private element

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The problem comes from the construction of Stream operations, which happens at the point a tagged type is frozen. Streams need to see the full view of types, so that for example the Read attribute for an array can be expanded into a loop over the Read attribute for the component type. Now if durin

[Ada] Fix missing error on actual for In/Out parameter

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The compiler was failing to give an error on the result of a call to the Input attribute passed as actual for an In/Out parameter. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.adb (Is_OK_Variable_For_Out_Formal): Remove test on Comes_From_Source in the co

[Ada] Fix indentation of "Start of processing for ..." labels

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The "Start of processing for ..." labels should be aligned with the BEGIN that follows. Violations found with: $ grep -Pzo "( *) \-\- Start of processing for \w+\n\n\1begin" *.adb and corrected manually, because some of them had to be entirely removed. Also, remove trailing semicolons found w

[Ada] Improve error messages to include full package name

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
This patch improves error messages in the compiler so that missing 'with' error messages show the complete package name instead of a limited number of selectors. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * err_vars.ads: Add new error message names and nodes. * er

[Ada] Remove redundant guards for empty list

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Routine Has_Excluded_Declaration iterates over declarations with First/Present/Next, which is safe when declarations are No_List. Cleanup related to excessive inlining-for-proof by GNATprove. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * inline.adb (Build_Body_To_Inline):

[Ada] Set Error_Msg_Warn before use of << insertion

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Calls to Error_Msg procedures with a message using the < or << insertions need to set appropriately Error_Msg_Warn. This was not done in one call, which would lead to spurious errors when changing the implementation of a runtime unit. This fixes it so that changes can be applied. Tested on x86_64-

[Ada] Prevent inlining-for-proof for calls inside ELSIF condition

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
In GNATprove we don't want inlining-for-proof to expand subprogram bodies into actions attached to nodes. These actions are attached either to expressions or to statements. For expressions, we prevented inlining by Is_Potentially_Unevaluated. For statements, we prevented inlining by In_While_Loop_

[Ada] Remove CodePeer annotations for pragma Loop_Variant

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Pragma Loop_Variant is now expanded into a null statement in CodePeer mode. Remove annotation related to false positives in runtime units. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-expmod.adb: Remove CodePeer annotation for pragma Loop_Variant.diff --

[Ada] Fully qualify name in JSON representation info

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
The current termination condition of the recursion is wrong. When in JSON mode, names should be fully qualified. This requires to stop not at the first encountered compilation unit but to recurse up to Standard. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * repinfo.adb (L

[Ada] Remove extra space around binary operators

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Style cleanups. Violation initially spotted while reading the code for UI_Expon; other occurrences found with grep (and examined manually, because sometimes the extra space is needed for a code layout). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * bindgen.adb, errout.adb,

[Ada] Simplify conversions from Uint to Char_Code

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Replace "Char_Code (UI_To_Int (...))" with "UI_To_CC (...). Cleanup related to handling characters in GNATprove counterexamples; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * par-prag.adb (Prag): Simplify conversion of character codes. * s

[Ada] Fix invalid memory access on finalization of class-wide type

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
This patch corrects issues in the compiler whereby finalization of a heap- allocated class-wide type may cause an invalid memory read at runtime when the type in question contains a component whose type has a large alignment. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * e

[Ada] Raise Constraint_Error when converting negative values to Char_Code

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
GNATprove relies on the comment for Get_Enum_Lit_From_Pos, which promises to raise Constraint_Error when its Pos parameter is not among the representation values for enumeration literal. However, this promise was only respected in builds with range checks enabled. The root problem was that a simil

[Ada] Suggest use of First_Valid/Last_Valid on type with static predicate

2022-05-09 Thread Pierre-Marie de Rodat via Gcc-patches
Attributes First_Valid/Last_Valid can be used on types with static predicate, instead of First/Last/Range. Include that suggestion in the corresponding error message. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.adb (Bad_Predicated_Subtype_Use): Add continuation

[Ada] Simplify conversion from Character to Char_Code

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Replace "Char_Code (Character'Pos (...))" with "Get_Char_Code (...)". The Get_Char_Code routine is inlined, so there is no performance penalty when it is called with static actual parameters. The N_Character_Literal has field Char_Literal_Value of type Unat, but we should really only store there v

[Ada] Fix comment about building names in task arrays

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Cleanup related to handling of character values in SPARK counterexamples, which just like the code for names in task arrays create N_Character_Literal nodes. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_util.adb (Build_Task_Array_Image): Fix style in the struc

[Ada] Failure compiling "for ... of" loop over a slice

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
In some cases involving a "for ... of" loop (not to be confused with the more common "for ... in" loop) iterating over a slice, compilation would fail with an internal compiler error. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.adb (Get_Actual_Subtype): If a new

[Ada] Fix incorrect range computation

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
When the type range [Lo, Hi] and the computed expression range [Lor, Hir] are disjoint, the range-constraining logic breaks and returns an incorrect range. For example, when Lodiff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -5469,22 +5469,49

[Ada] Replace variables with constants in expanded code for task names

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Using constants instead of variables is cleaner both in human-written and auto-generated code. Cleanup related to handling of character values in SPARK counterexamples, which just like the code for names of tasks create N_Character_Literal nodes. Tested on x86_64-pc-linux-gnu, committed on trunk

[Ada] Reject numeric literals with too big exponents

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
While the compiler can compute numeric literal with arbitrary large exponents, this may take ages and is most likely a typo. Better emit an error when we certainly expect it to take long. The chosen threshold takes about 100s to compute. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/

[Ada] Avoid repeated conversions from Int to Char_Code

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
When expanding aggregates like "(others => 'x')" into strings we repeated conversion from Int to Char_Code for every character. Now we convert once and use the Char_Code directly. Cleanup related to handling characters in GNATprove counterexamples; semantics is unaffected. Tested on x86_64-pc-li

[Ada] Fix oversight for case expression in Eval_Integer_Literal

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
The intent of the entry test is to treat conditional expressions, that is to say if-expression and case-expression, alike and to require that a second condition be true for them. But an N_Case_Expression_Alternative is not an N_Subexpr so this second condition was short-circuited for this node. T

[Ada] Fix hiding of user-defined operator that is not a homograph

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
This adds a missing test for the presence of a homograph when applying the RM 8.4(10) clause about the visibility of operators, and removes resolution code made obsolete by the change. There is also a fixlet for a previously undetected ambiguity in the runtime. Tested on x86_64-pc-linux-gnu, comm

[Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Add a new form of variants to ensure termination of loops or recursive subprograms. Structural variants correspond to objects which designate a part of the data-structure they used to designate in the previous loop iteration or recursive call. They only imply termination if the data-structure is ac

[Ada] Check if- and case-expressions for unset references

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Detection of references to unset (uninitialized) objects requires calls to Check_Unset_Reference on every subexpression of a composite statement and expression. This was missing for if-expressions and incomplete for case-expressions. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/

[Ada] Check declare and qualified expressions for unset references

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Detection of references to unset (uninitialized) objects requires calls to Check_Unset_Reference on every subexpression of a composite statement and expression. For declare and qualified expressions this was done only when they occurred within another composite statement/expression. Tested on x86_

[Ada] Refine iteration from entities to formals

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
When matching formal parameters from spec and body it is cleaner and more efficient to iterate with First_Formal/Next_Formal and not with First_Entity/Next_Entity. The previous iteration could unintentionally pick entities from within the subprogram body, e.g. objects declared within the subprogram

[Ada] Cleanup unnecessary declare block in Check_Unreachable_Code

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Cleanup related to static detection of references to uninitialized variables. Semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch5.adb (Check_Unreachable_Code): Remove inner declare block; refill code and comments.diff --git a/gcc/ada/sem_

[Ada] Remove tiny and incomplete optimization for unset references

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Code cleanup; behaviour is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.adb (Check_Unset_Reference): The early test was only saving time of calls to Original_Node, Comes_From_Source and Nkind, which are all quick and cheap.diff --git a

[Ada] Prevent search for references in postconditions from going too far

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Add a standard prevention against climbing the entire compilation unit. Cleanup only; behaviour of the compiler is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.adb (Within_Postcondition): Guard against search going too far.diff --git a/gcc/ada

[Ada] Cleanup detection of No_Elist with No and Present

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Replace equality and inequality operators with calls to No and Present. Offending occurrences found with: $ grep -n " /\?= No_Elist" *.adb Code cleanup only; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch11.adb, exp_ch5.adb, exp_prag.adb, g

[Ada] Reuse Is_Rewrite_Substitution where possible

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Replace comparisons of Original_Node with semantically equivalent but high-level calls to Is_Rewrite_Substitution. Offending occurrences found with: $ grep -n "Original_Node (\([A-Za-z_]\+\)) /\?= \1" *.adb Code cleanup only; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on

[Ada] Remove repeated conversions between Source_Ptr and Int

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Both Source_Ptr and Int are integer types (and even happen to have equal ranges). Their values can be calculated without converting back-and-forth, e.g.: Int (Loc1) - Int (Loc2) can be written simply as: Int (Loc1 - Loc2) Code cleanup related to handling of references to unset objects. Offe

[Ada] Optimize nonstandard boolean conversions

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
This patch improves the generated code for nonstandard boolean types. One of the improvements extends the code that avoids converting back to the nonstandard boolean type an expression computed as standard boolean, when it will be converted to a(nother) nonstandard boolean type. The other improve

[Ada] Simplify call to overloaded Earlier_In_Extended_Unit

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
We have two variants of Earlier_In_Extended_Unit that take either Node_Id or Source_Ptr values. The caller can simply use another variant and not explicitly convert parameters. Code cleanup; semantics is unaffected. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_warn.a

[Ada] Optimize nonstandard boolean validity checking

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
Validity checking of enumerations with nonstandard representation starts by checking the value range, then calling _rep_to_pos to verify that the value itself is valid. The value range check is thus redundant and inefficient: the _rep_to_pos call is normally inlined when optimizing for speed and th

[Ada] Incorrect ineffective use type clause warning

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
This patch fixes an issue in the compiler whereby a use_type_clause incorrectly gets flagged as ineffective when the use of it comes after a generic package instantiation where the installation of private use clauses are required and one such clause references the same type. Tested on x86_64-pc-li

[Ada] Handle non-standard booleans in if_expression condition

2022-05-10 Thread Pierre-Marie de Rodat via Gcc-patches
We failed to call Adjust_Condition for the condition expression of an if_expression, so non-standard booleans were expanded like standard booleans, disregarding representation clauses. Fixed. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * exp_ch4.adb (Expand_N_If_Expression

[Ada] Avoid crash for -gnatR -gnatc

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
If the -gnatR -gnatc are both given, then the compiler crashes. This patch fixes that, and avoids printing the uncomputed sizes and alignments that were causing the crash. (Previous versions of the compiler printed incorrect values in such cases.) Tested on x86_64-pc-linux-gnu, committed on trunk

[Ada] Set_Is_Known_Valid only if Safe_To_Capture_Value

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
Library-level variables with initializers could have Is_Known_Valid set when analyzing their definition, and the flag would only be cleared when analyzing a statement that assigned to them. Procedures and functions analyzed before the flag got cleared could skip validity checking for the correspond

[Ada] Move Reachable flag to E_Label entities

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
An entity flag Reachable is described as "defined in labels". It is only read and written for entities of kind E_Label (the code has necessary guards for that). There no need for this flag to be specified for all entities in the generated AST. Cleanup related to detection of uninitialized scalars

[Ada] Properly reject unsupported address specifications

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
In the case of an object declaration with an indefinite nominal subtype (roughly speaking, that's an object that takes its bounds, discriminants, and/or tag from its explicit initial value), GNAT does not support address specifications unless the size of the object is known at compile time. In som

[Ada] Add guard for making only legal labels unreachable

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
An entity flag Reachable now only applies to E_Label entities. We had an appropriate guard for setting this flag, but not for clearing. Cleanup related to detection of uninitialized scalars with GOTO statements. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_ch5.adb (A

[Ada] Document pragma Ada_2022

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
Pragma Ada_2022 is similar to existing pragma Ada_2012 and similarly deserves to be documented. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_pragmas.rst (Pragma Ada_2022): Copy description from pragma Ada 2012 and adapt.

[Ada] Fix markup in description of pragma Eliminate

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
Fix formatting of a nested bullet lists. Spotted while adding description of pragma Ada_2022. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_pragmas.rst (Pragma Eliminate): Fix markup. * gnat_rm.texi: Regenerate.diff --git

[Ada] Fix markup in description of implementation-defined characteristics

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
Fix formatting of description lists, i.e. continuation lines are now indented like their preceding lines. Spotted while adding description of pragma Ada_2022. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_characteristics.rst: Remove

[Ada] Fix layout in description of aspects and pragmas

2022-05-11 Thread Pierre-Marie de Rodat via Gcc-patches
Remove extra whitespace in examples of pragmas and aspects. Spotted while adding description of pragma Ada_2022. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_aspects.rst, doc/gnat_rm/implementation_defined_pragmas.rst: Remove ex

<    23   24   25   26   27   28   29   30   31   32   >