sem_spark.adb
185 KB
-
[Ada] Adapt ownership checking in SPARK to traversal functions · a2119175
A traversal function, especially when implemented as an expression function, may need to return an if-expression or case-expression, while still respecting Legality Rule SPARK RM 3.10(5). This case is now allowed in GNATprove. There is no impact on compilation. 2019-07-22 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_spark.adb (Get_Root_Object, Is_Path_Expression, Is_Subpath_Expression): Add parameter Is_Traversal to adapt these functions to the case of paths returned from a traversal function. (Read_Indexes): Handle the case of an if-expression or case-expression. (Check_Statement): Check Emit_Messages only when issuing an error message. This is important as Emit_Messages may store the information that an error was detected. From-SVN: r273693
Yannick Moy committed