aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gcc/ada/ChangeLog26
-rw-r--r--gcc/ada/adaint.c28
-rw-r--r--gcc/ada/exp_spark.adb53
-rw-r--r--gcc/ada/libgnarl/a-exetim__darwin.adb1
-rw-r--r--gcc/ada/libgnarl/s-intman__vxworks.adb1
-rw-r--r--gcc/ada/libgnarl/s-osinte__darwin.adb1
-rw-r--r--gcc/ada/libgnarl/s-osinte__lynxos178.adb2
-rw-r--r--gcc/ada/libgnat/a-strunb.adb2
-rw-r--r--gcc/ada/libgnat/a-stwiun.adb2
-rw-r--r--gcc/ada/libgnat/a-stzunb.adb2
-rw-r--r--gcc/ada/libgnat/g-socthi__vxworks.ads2
-rw-r--r--gcc/ada/libgnat/s-stchop__vxworks.adb2
-rw-r--r--gcc/ada/sem_ch3.adb8
-rw-r--r--gcc/ada/sem_ch5.adb10
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 <moy@adacore.com>
+
+ * 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 <bernardi@adacore.com>
+
+ * 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 <fofanov@adacore.com>
+
+ * 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 <moy@adacore.com>
+
+ * 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 <trojanek@adacore.com>
* 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;
generated by cgit v1.1 at 2024-10-06 16:28:39 +0000