+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
DWORD res;
int hl_len;
int found;
+ int pos;
START_WAIT:
/* -------------------- 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);
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 */
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);
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
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 --
------------------
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 =>
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 --
---------------------------------------
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;
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;
package body System.Interrupt_Management is
use System.OS_Interface;
- use type Interfaces.C.int;
-----------------------
-- Local Subprograms --
package body System.OS_Interface is
use Interfaces.C;
- use Interfaces.C.Extensions;
-----------------
-- To_Duration --
package body System.OS_Interface is
- use Interfaces.C;
-
------------------
-- Current_CPU --
------------------
package body Ada.Strings.Unbounded is
- use Ada.Finalization;
-
---------
-- "&" --
---------
package body Ada.Strings.Wide_Unbounded is
- use Ada.Finalization;
-
---------
-- "&" --
---------
package body Ada.Strings.Wide_Wide_Unbounded is
- use Ada.Finalization;
-
---------
-- "&" --
---------
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
--------------------------------------
procedure Set_Stack_Limit_For_Current_Task is
- use Interfaces.C;
-
type OS_Stack_Info is record
Size : Interfaces.C.int;
Base : System.Address;
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;
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;
projects / gcc.git / commitdiff