+2015-10-27 Javier Miranda <miranda@adacore.com>
+
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve previous patch.
+
+2015-10-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch12.adb (Analyze_Formal_Package_Declaration): Code cleanup. Set
+ and restore the value of global flag Ignore_Pragma_SPARK_Mode. A
+ formal package declaration acts as a package instantation with
+ respect to SPARK_Mode legality.
+
+2015-10-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Check_Constituent_Usage): Use
+ logical operators rather than short circuit operators. Emit an
+ error when a state with visible refinement is not refined.
+ * snames.ads-tmpl: Add names for detecting
+ predefined potentially blocking subprograms.
+
+2015-10-27 Arnaud Charlet <charlet@adacore.com>
+
+ * exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Revert previous
+ change.
+ (Expand_Array_Aggregate): Rewrite previous change here
+ as done for other non GCC back-ends.
+ (Build_Record_Aggr_Code): Add special case.
+
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Add_Item_To_Name_Buffer): Update the comment on usage.
end if;
end if;
- Instr :=
- Make_OK_Assignment_Statement (Loc,
- Name => Comp_Expr,
- Expression => Expr_Q);
+ if Generate_C_Code
+ and then Nkind (Expr_Q) = N_Aggregate
+ and then Is_Array_Type (Etype (Expr_Q))
+ and then Present (First_Index (Etype (Expr_Q)))
+ then
+ declare
+ Expr_Q_Type : constant Node_Id := Etype (Expr_Q);
+ begin
+ Append_List_To (L,
+ Build_Array_Aggr_Code
+ (N => Expr_Q,
+ Ctype => Component_Type (Expr_Q_Type),
+ Index => First_Index (Expr_Q_Type),
+ Into => Comp_Expr,
+ Scalar_Comp => Is_Scalar_Type
+ (Component_Type (Expr_Q_Type))));
+ end;
+
+ else
+ Instr :=
+ Make_OK_Assignment_Statement (Loc,
+ Name => Comp_Expr,
+ Expression => Expr_Q);
- Set_No_Ctrl_Actions (Instr);
- Append_To (L, Instr);
+ Set_No_Ctrl_Actions (Instr);
+ Append_To (L, Instr);
+ end if;
-- Adjust the tag if tagged (because of possible view
-- conversions), unless compiling for a VM where tags are
-- Backend processing by Gigi/gcc is possible only if all the following
-- conditions are met:
- -- 0. We are not generating C code
-
-- 1. N consists of a single OTHERS choice, possibly recursively
-- 2. The array type is not packed
Nunits : Nat;
begin
- if Generate_C_Code then
- return False;
- end if;
-
-- Recurse as far as possible to find the innermost component type
Ctyp := Etype (N);
if (In_Place_Assign_OK_For_Declaration or else Maybe_In_Place_OK)
and then not AAMP_On_Target
- and then not Generate_SCIL
+ and then not CodePeer_Mode
+ and then not Generate_C_Code
and then not Possible_Bit_Aligned_Component (Target)
and then not Is_Possibly_Unaligned_Slice (Target)
and then Aggr_Assignment_OK_For_Backend (N)
----------------------------------------
procedure Analyze_Formal_Package_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Pack_Id : constant Entity_Id := Defining_Identifier (N);
- Formal : Entity_Id;
- Gen_Id : constant Node_Id := Name (N);
- Gen_Decl : Node_Id;
- Gen_Unit : Entity_Id;
- New_N : Node_Id;
- Parent_Installed : Boolean := False;
- Renaming : Node_Id;
- Parent_Instance : Entity_Id;
- Renaming_In_Par : Entity_Id;
- Associations : Boolean := True;
+ Gen_Id : constant Node_Id := Name (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ Pack_Id : constant Entity_Id := Defining_Identifier (N);
+ Formal : Entity_Id;
+ Gen_Decl : Node_Id;
+ Gen_Unit : Entity_Id;
+ Renaming : Node_Id;
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
- -- to match the visibility of the formal type
+ -- to match the visibility of the formal type.
function Build_Local_Package return Node_Id;
-- The formal package is rewritten so that its parameters are replaced
return Pack_Decl;
end Build_Local_Package;
+ -- Local variables
+
+ Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
+ Associations : Boolean := True;
+ New_N : Node_Id;
+ Parent_Installed : Boolean := False;
+ Parent_Instance : Entity_Id;
+ Renaming_In_Par : Entity_Id;
+
-- Start of processing for Analyze_Formal_Package_Declaration
begin
Formal := New_Copy (Pack_Id);
Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment);
- begin
- -- Make local generic without formals. The formals will be replaced
- -- with internal declarations.
+ -- Make local generic without formals. The formals will be replaced with
+ -- internal declarations.
+ begin
New_N := Build_Local_Package;
- -- If there are errors in the parameter list, Analyze_Associations
- -- raises Instantiation_Error. Patch the declaration to prevent
- -- further exception propagation.
+ -- If there are errors in the parameter list, Analyze_Associations
+ -- raises Instantiation_Error. Patch the declaration to prevent further
+ -- exception propagation.
exception
when Instantiation_Error =>
-
Enter_Name (Formal);
Set_Ekind (Formal, E_Variable);
Set_Etype (Formal, Any_Type);
Append_Entity (Renaming_In_Par, Parent_Instance);
end if;
+ -- A formal package declaration behaves as a package instantiation with
+ -- respect to SPARK_Mode "off". If the annotation is "off" or altogether
+ -- missing, set the global flag which signals Analyze_Pragma to ingnore
+ -- all SPARK_Mode pragmas within the generic_package_name.
+
+ if SPARK_Mode /= On then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
+
Analyze (Specification (N));
-- The formals for which associations are provided are not visible
Set_Has_Completion (Formal, True);
- -- Add semantic information to the original defining identifier.
- -- for ASIS use.
+ -- Add semantic information to the original defining identifier for ASIS
+ -- use.
Set_Ekind (Pack_Id, E_Package);
Set_Etype (Pack_Id, Standard_Void_Type);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Pack_Id);
end if;
+
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
end Analyze_Formal_Package_Declaration;
---------------------------------
-- that carries the return value.
if Present (Cloned_Body_For_C) then
- Replace (N,
+ Rewrite (N,
Build_Procedure_Body_Form (Spec_Id, Cloned_Body_For_C));
Analyze (N);
end if;
-- A pair of one Input and one Output constituent is a valid
-- completion.
- elsif In_Seen and then Out_Seen then
+ elsif In_Seen and Out_Seen then
null;
-- A single Output constituent is a valid completion only when
-- some of the other constituents are missing (SPARK RM 7.2.4(5)).
- elsif Has_Missing and then Out_Seen then
+ elsif Out_Seen and Has_Missing then
null;
+ -- The state lacks a completion
+
+ elsif not In_Seen and not In_Out_Seen and not Out_Seen then
+ SPARK_Msg_NE
+ ("missing global refinement of state &", N, State_Id);
+
+ -- Otherwise the state has a malformed completion where at least
+ -- one of the constituents has a different mode.
+
else
SPARK_Msg_NE
("global refinement of state & redefines the mode of its "
Name_Wide_Text_IO : constant Name_Id := N + $;
Name_Wide_Wide_Text_IO : constant Name_Id := N + $;
+ -- Names for detecting predefined potentially blocking subprograms
+
+ Name_Abort_Task : constant Name_Id := N + $;
+ Name_Bounded_IO : constant Name_Id := N + $;
+ Name_C_Streams : constant Name_Id := N + $;
+ Name_Complex_IO : constant Name_Id := N + $;
+ Name_Directories : constant Name_Id := N + $;
+ Name_Direct_IO : constant Name_Id := N + $;
+ Name_Dispatching : constant Name_Id := N + $;
+ Name_Editing : constant Name_Id := N + $;
+ Name_EDF : constant Name_Id := N + $;
+ Name_Reset_Standard_Files : constant Name_Id := N + $;
+ Name_Sequential_IO : constant Name_Id := N + $;
+ Name_Streams : constant Name_Id := N + $;
+ Name_Suspend_Until_True : constant Name_Id := N + $;
+ Name_Suspend_Until_True_And_Set_Deadline : constant Name_Id := N + $;
+ Name_Synchronous_Barriers : constant Name_Id := N + $;
+ Name_Task_Identification : constant Name_Id := N + $;
+ Name_Text_Streams : constant Name_Id := N + $;
+ Name_Unbounded_IO : constant Name_Id := N + $;
+ Name_Wait_For_Release : constant Name_Id := N + $;
+ Name_Yield : constant Name_Id := N + $;
+
-- Names of implementations of the distributed systems annex
First_PCS_Name : constant Name_Id := N + $;