From 61b1489667e08d7b1ef6672682906072df7bc369 Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Mon, 25 Sep 2017 09:51:49 +0000 Subject: [PATCH] [multiple changes] 2017-09-25 Yannick Moy * exp_spark.adb (Expand_SPARK_Indexed_Component, Expand_SPARK_Selected_Component): New procedures to insert explicit dereference if required. (Expand_SPARK): Call the new procedures. 2017-09-25 Patrick Bernardi * libgnat/a-stwiun.adb, libgnat/s-stchop__vxworks.adb, libgnat/g-socthi__vxworks.ads, libgnat/a-stzunb.adb, libgnat/a-strunb.adb, libgnarl/s-osinte__lynxos178.adb, libgnarl/s-intman__vxworks.adb, libgnarl/s-osinte__darwin.adb, libgnarl/a-exetim__darwin.adb: Removed ineffective use-clauses. 2017-09-25 Vasiliy Fofanov * adaint.c (win32_wait): Properly handle error and take into account the WIN32 limitation on the number of simultaneous wait objects. 2017-09-25 Yannick Moy * sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the invariant procedure in GNATprove mode. * sem_ch5.adb (Analyze_Assignment): Likewise. From-SVN: r253143 --- gcc/ada/ChangeLog | 26 ++++++++++++++++ gcc/ada/adaint.c | 28 +++++++++++++++-- gcc/ada/exp_spark.adb | 53 ++++++++++++++++++++++++++++++++ gcc/ada/libgnarl/a-exetim__darwin.adb | 1 - gcc/ada/libgnarl/s-intman__vxworks.adb | 1 - gcc/ada/libgnarl/s-osinte__darwin.adb | 1 - gcc/ada/libgnarl/s-osinte__lynxos178.adb | 2 -- gcc/ada/libgnat/a-strunb.adb | 2 -- gcc/ada/libgnat/a-stwiun.adb | 2 -- gcc/ada/libgnat/a-stzunb.adb | 2 -- gcc/ada/libgnat/g-socthi__vxworks.ads | 2 -- gcc/ada/libgnat/s-stchop__vxworks.adb | 2 -- gcc/ada/sem_ch3.adb | 8 +++-- gcc/ada/sem_ch5.adb | 10 +++--- 14 files changed, 117 insertions(+), 23 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 979748e..28fa8f1 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,29 @@ +2017-09-25 Yannick Moy + + * exp_spark.adb (Expand_SPARK_Indexed_Component, + Expand_SPARK_Selected_Component): New procedures to insert explicit + dereference if required. + (Expand_SPARK): Call the new procedures. + +2017-09-25 Patrick Bernardi + + * libgnat/a-stwiun.adb, libgnat/s-stchop__vxworks.adb, + libgnat/g-socthi__vxworks.ads, libgnat/a-stzunb.adb, + libgnat/a-strunb.adb, libgnarl/s-osinte__lynxos178.adb, + libgnarl/s-intman__vxworks.adb, libgnarl/s-osinte__darwin.adb, + libgnarl/a-exetim__darwin.adb: Removed ineffective use-clauses. + +2017-09-25 Vasiliy Fofanov + + * adaint.c (win32_wait): Properly handle error and take into account + the WIN32 limitation on the number of simultaneous wait objects. + +2017-09-25 Yannick Moy + + * sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the + invariant procedure in GNATprove mode. + * sem_ch5.adb (Analyze_Assignment): Likewise. + 2017-09-25 Piotr Trojanek * adabkend.adb (Call_Back_End): Fix wording of "front-end" and diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c index b1da3e2..10325b0 100644 --- a/gcc/ada/adaint.c +++ b/gcc/ada/adaint.c @@ -2551,6 +2551,7 @@ win32_wait (int *status) DWORD res; int hl_len; int found; + int pos; START_WAIT: @@ -2563,7 +2564,15 @@ win32_wait (int *status) /* -------------------- critical section -------------------- */ EnterCS(); + /* ??? We can't wait for more than MAXIMUM_WAIT_OBJECTS due to a Win32 + limitation */ + if (plist_length < MAXIMUM_WAIT_OBJECTS) hl_len = plist_length; + else + { + errno = EINVAL; + return -1; + } #ifdef CERT hl = (HANDLE *) xmalloc (sizeof (HANDLE) * hl_len); @@ -2586,6 +2595,13 @@ win32_wait (int *status) res = WaitForMultipleObjects (hl_len, hl, FALSE, INFINITE); + /* If there was an error, exit now */ + if (res == WAIT_FAILED) + { + errno = EINVAL; + return -1; + } + /* if the ProcListEvt has been signaled then the list of processes has been updated to add or remove a handle, just loop over */ @@ -2596,9 +2612,17 @@ win32_wait (int *status) goto START_WAIT; } - h = hl[res - WAIT_OBJECT_0]; + /* Handle two distinct groups of return codes: finished waits and abandoned + waits */ + + if (res < WAIT_ABANDONED_0) + pos = res - WAIT_OBJECT_0; + else + pos = res - WAIT_ABANDONED_0; + + h = hl[pos]; GetExitCodeProcess (h, &exitcode); - pid = pidl [res - WAIT_OBJECT_0]; + pid = pidl [pos]; found = __gnat_win32_remove_handle (h, -1); diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index d4b9436..811033e 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -58,6 +58,9 @@ package body Exp_SPARK is procedure Expand_SPARK_Freeze_Type (E : Entity_Id); -- Build the DIC procedure of a type when needed, if not already done + procedure Expand_SPARK_Indexed_Component (N : Node_Id); + -- Insert explicit dereference if required + procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); -- Perform object-declaration-specific expansion @@ -67,6 +70,9 @@ package body Exp_SPARK is procedure Expand_SPARK_Op_Ne (N : Node_Id); -- Rewrite operator /= based on operator = when defined explicitly + procedure Expand_SPARK_Selected_Component (N : Node_Id); + -- Insert explicit dereference if required + ------------------ -- Expand_SPARK -- ------------------ @@ -138,6 +144,12 @@ package body Exp_SPARK is Expand_SPARK_Freeze_Type (Entity (N)); end if; + when N_Indexed_Component => + Expand_SPARK_Indexed_Component (N); + + when N_Selected_Component => + Expand_SPARK_Selected_Component (N); + -- In SPARK mode, no other constructs require expansion when others => @@ -264,6 +276,20 @@ package body Exp_SPARK is end if; end Expand_SPARK_Freeze_Type; + ------------------------------------ + -- Expand_SPARK_Indexed_Component -- + ------------------------------------ + + procedure Expand_SPARK_Indexed_Component (N : Node_Id) is + P : constant Node_Id := Prefix (N); + T : constant Entity_Id := Etype (P); + begin + if Is_Access_Type (T) then + Insert_Explicit_Dereference (P); + Analyze_And_Resolve (P, Designated_Type (T)); + end if; + end Expand_SPARK_Indexed_Component; + --------------------------------------- -- Expand_SPARK_N_Object_Declaration -- --------------------------------------- @@ -445,4 +471,31 @@ package body Exp_SPARK is end if; end Expand_SPARK_Potential_Renaming; + ------------------------------------- + -- Expand_SPARK_Selected_Component -- + ------------------------------------- + + procedure Expand_SPARK_Selected_Component (N : Node_Id) is + P : constant Node_Id := Prefix (N); + Ptyp : constant Entity_Id := Underlying_Type (Etype (P)); + begin + if Present (Ptyp) + and then Is_Access_Type (Ptyp) + then + -- First set prefix type to proper access type, in case it currently + -- has a private (non-access) view of this type. + + Set_Etype (P, Ptyp); + + Insert_Explicit_Dereference (P); + Analyze_And_Resolve (P, Designated_Type (Ptyp)); + + if Ekind (Etype (P)) = E_Private_Subtype + and then Is_For_Access_Subtype (Etype (P)) + then + Set_Etype (P, Base_Type (Etype (P))); + end if; + end if; + end Expand_SPARK_Selected_Component; + end Exp_SPARK; diff --git a/gcc/ada/libgnarl/a-exetim__darwin.adb b/gcc/ada/libgnarl/a-exetim__darwin.adb index a417d91..cb3a55a 100644 --- a/gcc/ada/libgnarl/a-exetim__darwin.adb +++ b/gcc/ada/libgnarl/a-exetim__darwin.adb @@ -189,7 +189,6 @@ package body Ada.Execution_Time is SC : out Ada.Real_Time.Seconds_Count; TS : out Ada.Real_Time.Time_Span) is - use type Ada.Real_Time.Time; begin Ada.Real_Time.Split (Ada.Real_Time.Time (T), SC, TS); end Split; diff --git a/gcc/ada/libgnarl/s-intman__vxworks.adb b/gcc/ada/libgnarl/s-intman__vxworks.adb index 67f7db3..62f9711 100644 --- a/gcc/ada/libgnarl/s-intman__vxworks.adb +++ b/gcc/ada/libgnarl/s-intman__vxworks.adb @@ -37,7 +37,6 @@ package body System.Interrupt_Management is use System.OS_Interface; - use type Interfaces.C.int; ----------------------- -- Local Subprograms -- diff --git a/gcc/ada/libgnarl/s-osinte__darwin.adb b/gcc/ada/libgnarl/s-osinte__darwin.adb index dcac8c0..880c9b4 100644 --- a/gcc/ada/libgnarl/s-osinte__darwin.adb +++ b/gcc/ada/libgnarl/s-osinte__darwin.adb @@ -39,7 +39,6 @@ with Interfaces.C.Extensions; package body System.OS_Interface is use Interfaces.C; - use Interfaces.C.Extensions; ----------------- -- To_Duration -- diff --git a/gcc/ada/libgnarl/s-osinte__lynxos178.adb b/gcc/ada/libgnarl/s-osinte__lynxos178.adb index 50e9353..a6dc986 100644 --- a/gcc/ada/libgnarl/s-osinte__lynxos178.adb +++ b/gcc/ada/libgnarl/s-osinte__lynxos178.adb @@ -37,8 +37,6 @@ pragma Polling (Off); package body System.OS_Interface is - use Interfaces.C; - ------------------ -- Current_CPU -- ------------------ diff --git a/gcc/ada/libgnat/a-strunb.adb b/gcc/ada/libgnat/a-strunb.adb index 808e26a..0366806 100644 --- a/gcc/ada/libgnat/a-strunb.adb +++ b/gcc/ada/libgnat/a-strunb.adb @@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation; package body Ada.Strings.Unbounded is - use Ada.Finalization; - --------- -- "&" -- --------- diff --git a/gcc/ada/libgnat/a-stwiun.adb b/gcc/ada/libgnat/a-stwiun.adb index 85bc494..2449822 100644 --- a/gcc/ada/libgnat/a-stwiun.adb +++ b/gcc/ada/libgnat/a-stwiun.adb @@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation; package body Ada.Strings.Wide_Unbounded is - use Ada.Finalization; - --------- -- "&" -- --------- diff --git a/gcc/ada/libgnat/a-stzunb.adb b/gcc/ada/libgnat/a-stzunb.adb index 25c3b29..2492fec 100644 --- a/gcc/ada/libgnat/a-stzunb.adb +++ b/gcc/ada/libgnat/a-stzunb.adb @@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation; package body Ada.Strings.Wide_Wide_Unbounded is - use Ada.Finalization; - --------- -- "&" -- --------- diff --git a/gcc/ada/libgnat/g-socthi__vxworks.ads b/gcc/ada/libgnat/g-socthi__vxworks.ads index 9cb4018..ac8eddf 100644 --- a/gcc/ada/libgnat/g-socthi__vxworks.ads +++ b/gcc/ada/libgnat/g-socthi__vxworks.ads @@ -49,8 +49,6 @@ package GNAT.Sockets.Thin is package C renames Interfaces.C; - use type System.CRTL.ssize_t; - function Socket_Errno return Integer renames GNAT.OS_Lib.Errno; -- Returns last socket error number diff --git a/gcc/ada/libgnat/s-stchop__vxworks.adb b/gcc/ada/libgnat/s-stchop__vxworks.adb index 25b07db..99e0288 100644 --- a/gcc/ada/libgnat/s-stchop__vxworks.adb +++ b/gcc/ada/libgnat/s-stchop__vxworks.adb @@ -103,8 +103,6 @@ package body System.Stack_Checking.Operations is -------------------------------------- procedure Set_Stack_Limit_For_Current_Task is - use Interfaces.C; - type OS_Stack_Info is record Size : Interfaces.C.int; Base : System.Address; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 2d9caca..7e451fe 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -12755,9 +12755,13 @@ package body Sem_Ch3 is end if; -- A deferred constant is a visible entity. If type has invariants, - -- verify that the initial value satisfies them. + -- verify that the initial value satisfies them. This is not done in + -- GNATprove mode, as GNATprove handles invariant checks itself. - if Has_Invariants (T) and then Present (Invariant_Procedure (T)) then + if Has_Invariants (T) + and then Present (Invariant_Procedure (T)) + and then not GNATprove_Mode + then Insert_After (N, Make_Invariant_Call (New_Occurrence_Of (Prev, Sloc (N)))); end if; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index e72dc4b..d33d59a 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -839,14 +839,16 @@ package body Sem_Ch5 is Set_Referenced_Modified (Lhs, Out_Param => False); end if; - -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type - -- to one of its ancestors) requires an invariant check. Apply check - -- only if expression comes from source, otherwise it will be applied - -- when value is assigned to source entity. + -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type to + -- one of its ancestors) requires an invariant check. Apply check only + -- if expression comes from source, otherwise it will be applied when + -- value is assigned to source entity. This is not done in GNATprove + -- mode, as GNATprove handles invariant checks itself. if Nkind (Lhs) = N_Type_Conversion and then Has_Invariants (Etype (Expression (Lhs))) and then Comes_From_Source (Expression (Lhs)) + and then not GNATprove_Mode then Insert_After (N, Make_Invariant_Call (Expression (Lhs))); end if; -- 2.7.4