OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2011-09-02  Bob Duff  <duff@adacore.com>

	* sem_ch6.adb: (Check_Post_State): Suppress warning
	"postcondition refers only to pre-state" when the expression has not
	yet been analyzed, because it causes false alarms. This can happen when
	the postcondition contains a quantified expression, because those are
	analyzed later. This is a temporary/partial fix.
	(Process_Post_Conditions): Minor: change wording of warning.

2011-09-02  Marc Sango  <sango@adacore.com>

	* sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of
	illegal use of unconstrained string type in SPARK mode.
	* sem_res.adb (Analyze_Operator_Symbol): Set the
	right place where the string operand of concatenation should be
	violate in SPARK mode.

From-SVN: r178460
This commit is contained in:
Arnaud Charlet 2011-09-02 11:59:32 +02:00
parent bd603506f6
commit 5b5588dd53
4 changed files with 39 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
gcc/ada/ChangeLog
View File

@ -1,3 +1,20 @@
2011-09-02 Bob Duff <duff@adacore.com>
* sem_ch6.adb: (Check_Post_State): Suppress warning
"postcondition refers only to pre-state" when the expression has not
yet been analyzed, because it causes false alarms. This can happen when
the postcondition contains a quantified expression, because those are
analyzed later. This is a temporary/partial fix.
(Process_Post_Conditions): Minor: change wording of warning.
2011-09-02 Marc Sango <sango@adacore.com>
* sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of
illegal use of unconstrained string type in SPARK mode.
* sem_res.adb (Analyze_Operator_Symbol): Set the
right place where the string operand of concatenation should be
violate in SPARK mode.
2011-09-02 Robert Dewar <dewar@adacore.com>
* sem_prag.adb, sem_util.adb, sem_ch6.adb, prj-nmsc.adb,

9
gcc/ada/sem_ch3.adb
View File

@ -3313,9 +3313,18 @@ package body Sem_Ch3 is
-- Case of initialization present
else
-- Not allowed in Ada 83
if not Constant_Present (N) then
-- A declaration of unconstrained type in SPARK is limited,
-- the only exception to this is the admission of declaration
-- of constants of type string.
Check_SPARK_Restriction
("declaration of unconstrained type is limited", E);
if Ada_Version = Ada_83
and then Comes_From_Source (Object_Definition (N))
then

15
gcc/ada/sem_ch6.adb
View File

@ -5551,9 +5551,16 @@ package body Sem_Ch6 is
declare
E : constant Entity_Id := Entity (N);
begin
if Is_Entity_Name (N)
and then Present (E)
and then Ekind (E) in Assignable_Kind
-- ???Quantified expressions get analyzed later, so E can be
-- empty at this point. In this case, we suppress the
-- warning, just in case E is assignable. It seems better to
-- have false negatives than false positives. At some point,
-- we should make the warning more accurate, either by
-- analyzing quantified expressions earlier, or moving this
-- processing later.
if No (E) or else
(Is_Entity_Name (N) and then Ekind (E) in Assignable_Kind)
then
Found := True;
end if;
@ -5627,7 +5634,7 @@ package body Sem_Ch6 is
Ignored := Find_Post_State (Arg);
if not Post_State_Mentioned then
Error_Msg_N ("?postcondition only refers to pre-state",
Error_Msg_N ("?postcondition refers only to pre-state",
Prag);
end if;
end if;

4
gcc/ada/sem_res.adb
View File

@ -7741,7 +7741,7 @@ package body Sem_Res is
if Is_Character_Type (Etype (Arg)) then
if not Is_Static_Expression (Arg) then
Check_SPARK_Restriction
("character operand for concatenation should be static", N);
("character operand for concatenation should be static", Arg);
end if;
elsif Is_String_Type (Etype (Arg)) then
@ -7750,7 +7750,7 @@ package body Sem_Res is
and then not Is_Static_Expression (Arg)
then
Check_SPARK_Restriction
("string operand for concatenation should be static", N);
("string operand for concatenation should be static", Arg);
end if;
-- Do not issue error on an operand that is neither a character nor a