-2015-05-21 Robert Dewar <dewar@adacore.com>
+2015-05-22 Robert Dewar <dewar@adacore.com>
+
+ * a-reatim.ads: Add Compile_Time_Error to ensure Duration
+ is 64-bits.
+ * sem_ch13.adb: Improve error message.
+ * exp_ch4.adb: Minor reformatting.
+
+2015-05-22 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Analyze_Pragma): Constants without variable
+ input do not require indicator Part_Of.
+ (Check_Missing_Part_Of): Constants without variable input do not
+ requrie indicator Part_Of.
+ (Collect_Visible_States): Constants without variable input are
+ not part of the hidden state of a package.
+ * sem_util.ads, sem_util.adb (Has_Variable_Input): New routine.
+
+2015-05-22 Robert Dewar <dewar@adacore.com>
* exp_util.adb (Activate_Atomic_Synchronization): Do not set
Atomic_Sync_Required for an object renaming declaration.
* sem_ch8.adb (Analyze_Object_Renaming): Copy Is_Atomic and
Is_Independent to renaming object.
-2015-05-21 Ed Schonberg <schonberg@adacore.com>
+2015-05-22 Ed Schonberg <schonberg@adacore.com>
* sem_ch5.adb (Analyze_Iterator_Specification): Diagnose
various illegalities in iterators over arrays and containers:
package Ada.Real_Time is
+ pragma Compile_Time_Error
+ (Duration'Size /= 64,
+ "this version of Ada.Real_Time requires 64-bit Duration");
+
type Time is private;
Time_First : constant Time;
Time_Last : constant Time;
begin
if (Nkind (P) = N_Op_Multiply
- and then not Non_Binary_Modulus (Typ)
- and then
- ((Is_Integer_Type (Etype (L)) and then R = N)
- or else
- (Is_Integer_Type (Etype (R)) and then L = N))
- and then not Do_Overflow_Check (P))
+ and then not Non_Binary_Modulus (Typ)
+ and then
+ ((Is_Integer_Type (Etype (L)) and then R = N)
+ or else
+ (Is_Integer_Type (Etype (R)) and then L = N))
+ and then not Do_Overflow_Check (P))
+
or else
(Nkind (P) = N_Op_Divide
and then Is_Integer_Type (Etype (L))
end if;
end;
- -- Now the other cases
+ -- Now the other cases where we convert to 1 * (2 ** K)
elsif not Non_Binary_Modulus (Typ) then
Rewrite (N,
elsif No (Next_Formal (First_Formal (Subp))) then
Illegal_Indexing
- ("indexing function must have at least two parameters");
+ ("indexing function must have at least two parameters");
return;
elsif Is_Derived_Type (Ent) then
- if (Attr = Name_Constant_Indexing
- and then Present
- (Find_Aspect (Etype (Ent), Aspect_Constant_Indexing)))
- or else
- (Attr = Name_Variable_Indexing
- and then Present
- (Find_Aspect (Etype (Ent), Aspect_Variable_Indexing)))
- then
- if Debug_Flag_Dot_XX then
- null;
+ declare
+ Inherited : Node_Id;
- else
- Illegal_Indexing
- ("indexing function already inherited "
- & "from parent type");
- return;
+ begin
+ if Attr = Name_Constant_Indexing then
+ Inherited :=
+ Find_Aspect (Etype (Ent), Aspect_Constant_Indexing);
+ elsif Attr = Name_Variable_Indexing then
+ Inherited :=
+ Find_Aspect (Etype (Ent), Aspect_Variable_Indexing);
end if;
- end if;
+
+ -- What if neither branch taken above ???
+
+ if Present (Inherited) then
+ if Debug_Flag_Dot_XX then
+ null;
+
+ -- Indicate the operation that must be overridden,
+ -- rather than redefining the indexing aspect
+
+ else
+ Illegal_Indexing
+ ("indexing function already inherited "
+ & "from parent type");
+ Error_Msg_NE
+ ("!override& instead",
+ N, Entity (Expression (Inherited)));
+ return;
+ end if;
+ end if;
+ end;
end if;
if not Check_Primitive_Function (Subp) then
Legal : out Boolean);
-- Subsidiary to the analysis of pragmas Abstract_State and Part_Of.
-- Perform full analysis of indicator Part_Of. Item_Id is the entity of
- -- an abstract state, variable or package instantiation. State is the
+ -- an abstract state, object or package instantiation. State is the
-- encapsulating state. Indic is the Part_Of indicator. Flag Legal is
-- set when the indicator is legal.
Legal => Legal);
if Legal then
+
+ -- Constants without "variable input" are not considered part
+ -- of the hidden state of a package (SPARK RM 7.1.1(2)). As a
+ -- result such constants do not require a Part_Of indicator.
+
+ if Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ SPARK_Msg_NE
+ ("useless Part_Of indicator, constant & does not have "
+ & "variable input", N, Item_Id);
+ return;
+ end if;
+
State_Id := Entity (State);
-- The Part_Of indicator turns an object into a constituent of
-- formals to their actuals as the formals cannot be named
-- from the outside and participate in refinement.
- if No (Corresponding_Generic_Association (Decl)) then
+ if Present (Corresponding_Generic_Association (Decl)) then
+ null;
+
+ -- Constants without "variable input" are not considered a
+ -- hidden state of a package (SPARK RM 7.1.1(2)).
+
+ elsif Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ null;
+
+ else
Add_Item (Item_Id, Result);
end if;
elsif SPARK_Mode /= On then
return;
+
+ -- Do not consider constants without variable input because those are
+ -- not part of the hidden state of a package (SPARK RM 7.1.1(2)).
+
+ elsif Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ return;
end if;
-- Find where the abstract state, variable or package instantiation
end if;
end Has_Tagged_Component;
+ ------------------------
+ -- Has_Variable_Input --
+ ------------------------
+
+ function Has_Variable_Input (Const_Id : Entity_Id) return Boolean is
+ Expr : constant Node_Id := Expression (Declaration_Node (Const_Id));
+
+ begin
+ return
+ Present (Expr) and then not Compile_Time_Known_Value_Or_Aggr (Expr);
+ end Has_Variable_Input;
+
----------------------------
-- Has_Volatile_Component --
----------------------------
-- component is present. This function is used to check if "=" has to be
-- expanded into a bunch component comparisons.
+ function Has_Variable_Input (Const_Id : Entity_Id) return Boolean;
+ -- Determine whether the initialization expression of constant Const_Id has
+ -- "variable input" (SPARK RM 7.1.1(2)). This roughly maps to the semantic
+ -- concept of a compile-time known value.
+
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
-- Given an arbitrary type, determine whether it contains at least one
-- volatile component.