Commit 7b52257c by Arnaud Charlet

[multiple changes]

2015-11-25  Arnaud Charlet  <charlet@adacore.com>

	* exp_util.adb (Remove_Side_Effects): Minimize extra temporaries
	and use of 'Reference when needed.

2015-11-25  Doug Rupp  <rupp@adacore.com>

	* sigtramp-vxworks-target.inc (__x86_64__): Restore context for the
	sake of uniformity.
	* init.c (__gnat_inum_to_ivec): Add some casting to avoid
	warnings when sizeof(long) != sizeof(int)

2015-11-25  Yannick Moy  <moy@adacore.com>

	* lib-xref-spark_specific.adb (SPARK_Entities): Add entries for
	consideration.
	(Add_SPARK_Scope): Take tasks into account.
	(Detect_And_Add_SPARK_Scope): Take tasks into account.
	(Enclosing_Subprogram_Or_Library_Package): Take tasks into account.

From-SVN: r230878
parent e9c12b91
2015-11-25 Arnaud Charlet <charlet@adacore.com>
* exp_util.adb (Remove_Side_Effects): Minimize extra temporaries
and use of 'Reference when needed.
2015-11-25 Doug Rupp <rupp@adacore.com>
* sigtramp-vxworks-target.inc (__x86_64__): Restore context for the
sake of uniformity.
* init.c (__gnat_inum_to_ivec): Add some casting to avoid
warnings when sizeof(long) != sizeof(int)
2015-11-25 Yannick Moy <moy@adacore.com>
* lib-xref-spark_specific.adb (SPARK_Entities): Add entries for
consideration.
(Add_SPARK_Scope): Take tasks into account.
(Detect_And_Add_SPARK_Scope): Take tasks into account.
(Enclosing_Subprogram_Or_Library_Package): Take tasks into account.
2015-11-25 Bob Duff <duff@adacore.com> 2015-11-25 Bob Duff <duff@adacore.com>
* sem_elab.adb (Check_Internal_Call_Continue): Code clean ups. * sem_elab.adb (Check_Internal_Call_Continue): Code clean ups.
......
...@@ -7816,9 +7816,10 @@ package body Exp_Util is ...@@ -7816,9 +7816,10 @@ package body Exp_Util is
else else
-- An expression which is in SPARK mode is considered side effect -- An expression which is in SPARK mode is considered side effect
-- free if the resulting value is captured by a variable or a -- free if the resulting value is captured by a variable or a
-- constant. -- constant. Same reasoning when generating C code.
-- Why can't we apply this test in general???
if GNATprove_Mode if (GNATprove_Mode or Generate_C_Code)
and then Nkind (Parent (Exp)) = N_Object_Declaration and then Nkind (Parent (Exp)) = N_Object_Declaration
then then
goto Leave; goto Leave;
...@@ -7862,8 +7863,10 @@ package body Exp_Util is ...@@ -7862,8 +7863,10 @@ package body Exp_Util is
-- the secondary stack. Since SPARK (and why) cannot process access -- the secondary stack. Since SPARK (and why) cannot process access
-- types, use a different approach which ignores the secondary stack -- types, use a different approach which ignores the secondary stack
-- and "copies" the returned object. -- and "copies" the returned object.
-- When generating C code, no need for a 'reference since the
-- secondary stack is not supported.
if GNATprove_Mode then if GNATprove_Mode or Generate_C_Code then
Res := New_Occurrence_Of (Def_Id, Loc); Res := New_Occurrence_Of (Def_Id, Loc);
Ref_Type := Exp_Type; Ref_Type := Exp_Type;
...@@ -7898,10 +7901,10 @@ package body Exp_Util is ...@@ -7898,10 +7901,10 @@ package body Exp_Util is
else else
E := Relocate_Node (E); E := Relocate_Node (E);
-- Do not generate a 'reference in SPARK mode since the access -- Do not generate a 'reference in SPARK mode or C generation
-- type is not created in the first place. -- since the access type is not created in the first place.
if GNATprove_Mode then if GNATprove_Mode or Generate_C_Code then
New_Exp := E; New_Exp := E;
-- Otherwise generate reference, marking the value as non-null -- Otherwise generate reference, marking the value as non-null
......
...@@ -1732,7 +1732,7 @@ extern int __gnat_inum_to_ivec (int); ...@@ -1732,7 +1732,7 @@ extern int __gnat_inum_to_ivec (int);
int int
__gnat_inum_to_ivec (int num) __gnat_inum_to_ivec (int num)
{ {
return (int) INUM_TO_IVEC (num); return (int) ((long) INUM_TO_IVEC ((long) num));
} }
#endif #endif
...@@ -2115,9 +2115,9 @@ __gnat_init_float (void) ...@@ -2115,9 +2115,9 @@ __gnat_init_float (void)
#endif #endif
#endif #endif
#if defined (__i386__) && !defined (VTHREADS) #if (defined (__i386__) && !defined (VTHREADS))
/* This is used to properly initialize the FPU on an x86 for each /* This is used to properly initialize the FPU on an x86 for each
process thread. */ process thread. Is this needed for x86_64 ??? */
asm ("finit"); asm ("finit");
#endif #endif
......
...@@ -40,6 +40,7 @@ package body SPARK_Specific is ...@@ -40,6 +40,7 @@ package body SPARK_Specific is
SPARK_Entities : constant array (Entity_Kind) of Boolean := SPARK_Entities : constant array (Entity_Kind) of Boolean :=
(E_Constant => True, (E_Constant => True,
E_Entry => True,
E_Function => True, E_Function => True,
E_In_Out_Parameter => True, E_In_Out_Parameter => True,
E_In_Parameter => True, E_In_Parameter => True,
...@@ -268,7 +269,7 @@ package body SPARK_Specific is ...@@ -268,7 +269,7 @@ package body SPARK_Specific is
=> =>
Typ := Xref_Entity_Letters (Ekind (E)); Typ := Xref_Entity_Letters (Ekind (E));
when E_Package_Body | E_Subprogram_Body => when E_Package_Body | E_Subprogram_Body | E_Task_Body =>
Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
when E_Void => when E_Void =>
...@@ -1006,14 +1007,19 @@ package body SPARK_Specific is ...@@ -1006,14 +1007,19 @@ package body SPARK_Specific is
procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
begin begin
if Nkind_In (N, N_Entry_Body, if Nkind_In (N, N_Entry_Body, -- entries
N_Entry_Declaration, N_Entry_Declaration)
N_Package_Body, or else
Nkind_In (N, N_Package_Body, -- packages
N_Package_Body_Stub, N_Package_Body_Stub,
N_Package_Declaration, N_Package_Declaration)
N_Subprogram_Body, or else
Nkind_In (N, N_Subprogram_Body, -- subprograms
N_Subprogram_Body_Stub, N_Subprogram_Body_Stub,
N_Subprogram_Declaration) N_Subprogram_Declaration)
or else
Nkind_In (N, N_Task_Body, -- tasks
N_Task_Body_Stub)
then then
Add_SPARK_Scope (N); Add_SPARK_Scope (N);
end if; end if;
...@@ -1105,6 +1111,10 @@ package body SPARK_Specific is ...@@ -1105,6 +1111,10 @@ package body SPARK_Specific is
Result := Defining_Identifier (Result); Result := Defining_Identifier (Result);
exit; exit;
when N_Task_Body =>
Result := Defining_Identifier (Result);
exit;
when others => when others =>
Result := Parent (Result); Result := Parent (Result);
end case; end case;
......
...@@ -441,6 +441,7 @@ TCR("# Call the real handler. The signo, siginfo and sigcontext") \ ...@@ -441,6 +441,7 @@ TCR("# Call the real handler. The signo, siginfo and sigcontext") \
TCR("# arguments are the same as those we received") \ TCR("# arguments are the same as those we received") \
TCR("call *%rcx") \ TCR("call *%rcx") \
TCR("# This part should never be executed") \ TCR("# This part should never be executed") \
TCR("addq $8, %rsp") \
TCR("ret") TCR("ret")
#else #else
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment