[multiple changes]
2014-01-23 Robert Dewar <dewar@adacore.com> * opt.adb (Register_Opt_Config_Switches): Save SPARK_Mode_Pragma setting. 2014-01-23 Ed Schonberg <schonberg@adacore.com> * sem_util.adb (Is_Potentially_Unevaluated): Predicate only applies to expressions that come from source. * sem_attr.adb (Analyze_Attribute, case 'Old): Improve error message. (Analyze_Attribute, case 'Loop_Entry): Apply SPARK 2014 legality rule regarding potentially unevaluated expressions, to prefix of attribute. From-SVN: r206993
This commit is contained in:
parent
19992053df
commit
ea0f1fc8e4
|
@ -1,3 +1,18 @@
|
|||
2014-01-23 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* opt.adb (Register_Opt_Config_Switches): Save SPARK_Mode_Pragma
|
||||
setting.
|
||||
|
||||
2014-01-23 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_util.adb (Is_Potentially_Unevaluated): Predicate only
|
||||
applies to expressions that come from source.
|
||||
* sem_attr.adb (Analyze_Attribute, case 'Old): Improve error
|
||||
message.
|
||||
(Analyze_Attribute, case 'Loop_Entry): Apply SPARK 2014 legality
|
||||
rule regarding potentially unevaluated expressions, to prefix
|
||||
of attribute.
|
||||
|
||||
2014-01-23 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* exp_util.adb (Make_Invqriant_Call): If type of expression is
|
||||
|
|
|
@ -64,6 +64,7 @@ package body Opt is
|
|||
Polling_Required_Config := Polling_Required;
|
||||
Short_Descriptors_Config := Short_Descriptors;
|
||||
SPARK_Mode_Config := SPARK_Mode;
|
||||
SPARK_Mode_Pragma_Config := SPARK_Mode_Pragma;
|
||||
Use_VADS_Size_Config := Use_VADS_Size;
|
||||
|
||||
-- Reset the indication that Optimize_Alignment was set locally, since
|
||||
|
|
|
@ -3994,13 +3994,23 @@ package body Sem_Attr is
|
|||
Check_References_In_Prefix (Loop_Id);
|
||||
|
||||
-- The prefix must denote a static entity if the pragma does not
|
||||
-- apply to the innermost enclosing loop statement.
|
||||
-- apply to the innermost enclosing loop statement, or if it appears
|
||||
-- within a potentially unevaluated epxression.
|
||||
|
||||
if Present (Enclosing_Loop)
|
||||
and then Entity (Identifier (Enclosing_Loop)) /= Loop_Id
|
||||
and then not Is_Entity_Name (P)
|
||||
if Is_Entity_Name (P)
|
||||
or else Nkind (Parent (P)) = N_Object_Renaming_Declaration
|
||||
then
|
||||
Error_Attr_P ("prefix of attribute % must denote an entity");
|
||||
null;
|
||||
|
||||
elsif Present (Enclosing_Loop)
|
||||
and then Entity (Identifier (Enclosing_Loop)) /= Loop_Id
|
||||
then
|
||||
Error_Attr_P ("prefix of attribute % that applies to "
|
||||
& "outer loop must denote an entity");
|
||||
|
||||
elsif Is_Potentially_Unevaluated (P) then
|
||||
Error_Attr_P ("prefix of attribute % that is potentially "
|
||||
& "unevaluated must denote an entity");
|
||||
end if;
|
||||
end Loop_Entry;
|
||||
|
||||
|
@ -4525,9 +4535,8 @@ package body Sem_Attr is
|
|||
and then Is_Potentially_Unevaluated (N)
|
||||
and then not Is_Entity_Name (P)
|
||||
then
|
||||
Error_Msg_N
|
||||
("prefix that is potentially unevaluated must denote an entity",
|
||||
N);
|
||||
Error_Attr_P ("prefix of attribute % that is potentially "
|
||||
& "unevaluated must denote an entity");
|
||||
end if;
|
||||
|
||||
-- The attribute appears within a pre/postcondition, but refers to
|
||||
|
|
|
@ -10334,7 +10334,13 @@ package body Sem_Util is
|
|||
Expr := Par;
|
||||
Par := Parent (Par);
|
||||
|
||||
if Nkind (Par) not in N_Subexpr then
|
||||
-- If the context is not an expression, or if is the result of
|
||||
-- expansion of an enclosing construct (such as another attribute)
|
||||
-- the predicate does not apply.
|
||||
|
||||
if Nkind (Par) not in N_Subexpr
|
||||
or else not Comes_From_Source (Par)
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
end loop;
|
||||
|
|
Loading…
Reference in New Issue