aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorArnaud Charlet <charlet@gcc.gnu.org>2011-09-05 15:40:04 +0200
committerArnaud Charlet <charlet@gcc.gnu.org>2011-09-05 15:40:04 +0200
commit9ec080cb2152ca831307b8c4fd825d9acecc4a45 (patch)
treef6cdb02884910b21f8b1c6e72a3d780e87a56745
parent94bbf008bae624219030c93f6b74def28677e0a7 (diff)
downloadgcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.zip
gcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.tar.gz
gcc-9ec080cb2152ca831307b8c4fd825d9acecc4a45.tar.bz2
[multiple changes]
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. From-SVN: r178538
-rw-r--r--gcc/ada/ChangeLog15
-rw-r--r--gcc/ada/lib-xref-alfa.adb38
-rw-r--r--gcc/ada/sem_ch3.adb23
-rw-r--r--gcc/ada/sem_ch5.adb7
4 files changed, 51 insertions, 32 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 22d261d..e267e9b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+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,
diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb
index 8eef505..cc0aa3a 100644
--- a/gcc/ada/lib-xref-alfa.adb
+++ b/gcc/ada/lib-xref-alfa.adb
@@ -586,10 +586,12 @@ package body Alfa is
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
@@ -604,35 +606,33 @@ package body Alfa is
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;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 46abaa9..2953141 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3267,6 +3267,16 @@ package body Sem_Ch3 is
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
@@ -3313,21 +3323,10 @@ package body Sem_Ch3 is
-- 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
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 5a2d2b3..81153fa 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2336,13 +2336,18 @@ package body Sem_Ch5 is
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;