* sem_ch3.adb (Analyze_Object_Declaration): Remove
the wrong test and add the correct test to detect the violation
of illegal use of unconstrained string type in SPARK mode.
2011-09-05 Ed Schonberg <schonberg@adacore.com>
* sem_ch5.adb (Analyze_Iteration_Specification): Improve error
message on an iterator over an array.
2011-09-05 Robert Dewar <dewar@adacore.com>
* lib-xref-alfa.adb: Minor reformatting.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@178538
138bc75d-0d04-0410-961f-
82ee72b054a4
+2011-09-05 Marc Sango <sango@adacore.com>
+
+ * sem_ch3.adb (Analyze_Object_Declaration): Remove
+ the wrong test and add the correct test to detect the violation
+ of illegal use of unconstrained string type in SPARK mode.
+
+2011-09-05 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch5.adb (Analyze_Iteration_Specification): Improve error
+ message on an iterator over an array.
+
+2011-09-05 Robert Dewar <dewar@adacore.com>
+
+ * lib-xref-alfa.adb: Minor reformatting.
+
2011-09-05 Robert Dewar <dewar@adacore.com>
* sem_ch3.adb, sem_res.adb, par.adb, par-ch6.adb, g-comlin.adb,
function Is_Alfa_Reference
(E : Entity_Id;
Typ : Character) return Boolean;
- -- Return whether the reference is adequate for this entity
+ -- Return whether entity reference E meets Alfa requirements. Typ
+ -- is the reference type.
function Is_Alfa_Scope (E : Entity_Id) return Boolean;
- -- Return whether the entity or reference scope is adequate
+ -- Return whether the entity or reference scope meets requirements
+ -- for being an Alfa scope.
function Is_Global_Constant (E : Entity_Id) return Boolean;
-- Return True if E is a global constant for which we should ignore
Typ : Character) return Boolean
is
begin
+ -- The only references of interest on callable entities are calls.
+ -- On non-callable entities, the only references of interest are
+ -- reads and writes.
if Ekind (E) in Overloadable_Kind then
-
- -- The only references of interest on callable entities are
- -- calls. On non-callable entities, the only references of
- -- interest are reads and writes.
-
return Typ = 's';
- elsif Is_Constant_Object (E) then
-
- -- References to constant objects are not considered in Alfa
- -- section, as these will be translated as constants in the
- -- intermediate language for formal verification, and should
- -- therefore never appear in frame conditions.
+ -- References to constant objects are not considered in Alfa
+ -- section, as these will be translated as constants in the
+ -- intermediate language for formal verification, and should
+ -- therefore never appear in frame conditions.
+ elsif Is_Constant_Object (E) then
return False;
- elsif Present (Etype (E)) and then
- Ekind (Etype (E)) in Concurrent_Kind then
-
- -- Objects of Task type or protected type are not Alfa
- -- references.
+ -- Objects of Task type or protected type are not Alfa references
+ elsif Present (Etype (E))
+ and then Ekind (Etype (E)) in Concurrent_Kind
+ then
return False;
+ -- In all other cases, result is true for reference/modify cases,
+ -- and false for all other cases.
+
else
return Typ = 'r' or else Typ = 'm';
-
end if;
end Is_Alfa_Reference;
if Is_Indefinite_Subtype (T) then
+ -- In SPARK, a declaration of unconstrained type is allowed
+ -- only for constants of type string.
+
+ if Is_String_Type (T)
+ and then not Constant_Present (Original_Node (N)) then
+ Check_SPARK_Restriction
+ ("declaration of object of unconstrained type not allowed",
+ N);
+ end if;
+
-- Nothing to do in deferred constant case
if Constant_Present (N) and then No (E) then
-- Case of initialization present
else
- -- Check restrictions in Ada 83 and SPARK modes
+ -- Check restrictions in Ada 83
if not Constant_Present (N) then
- -- In SPARK, a declaration of unconstrained type is allowed
- -- only for constants of type string.
-
- -- Isn't following check the wrong way round???
-
- if Nkind (E) = N_String_Literal then
- Check_SPARK_Restriction
- ("declaration of object of unconstrained type not allowed",
- E);
- end if;
-
-- Unconstrained variables not allowed in Ada 83 mode
if Ada_Version = Ada_83
if Is_Array_Type (Typ) then
if Of_Present (N) then
Set_Etype (Def_Id, Component_Type (Typ));
+
+ elsif Ada_Version < Ada_2012 then
+ Error_Msg_N
+ ("missing Range attribute in iteration over an array", N);
+
else
Error_Msg_N
("to iterate over the elements of an array, use OF", N);
-- Prevent cascaded errors
- Set_Ekind (Def_Id, E_Constant);
+ Set_Ekind (Def_Id, E_Loop_Parameter);
Set_Etype (Def_Id, Etype (First_Index (Typ)));
end if;