[Ada] Refactor ownership pointer checking in SPARK as a generic

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 11 July 2019 08:03 EDT

Ownership checking as done in SPARK should be applied only to SPARK code, which requires GNATprove knowledge of the SPARK_Mode boundary. Transform the checking unit into a generic to allow passing in the knowledge from GNATprove to that unit in GNAT sources.

Keeping the code in GNAT sources makes it possible in the future to adapt it further (or simply instantiate it differently) to be used on Ada code, independently of GNATprove.

There is no impact on compilation.

2019-07-11 Claire Dross

gcc/ada/

- gnat1drv.adb: SPARK checking rules for pointer aliasing are moved to GNATprove backend.
- sem_spark.ads, sem_spark.adb (Sem_SPARK): Is now a generic unit. Takes as parameters:- Retysp which is used to query the most underlying type
visible in SPARK. We do not introduce aliasing checks for types which are not visibly deep.- Component_Is_Visible_In_SPARK is used to avoid doing pointer aliasing checks on components which are not visible in SPARK.- Emit_Messages returns True in the second phase of SPARK analysis. Error messages for failed aliasing checks are only output in this case. Additionally, errors on constructs not supported in SPARK are removed as duplicates of marking errors. Components are stored in the permission map using their original component to avoid inconsistencies between components of different views of the same type. (Check_Expression): Handle delta constraints. (Is_Deep): Exported so that we can check for SPARK restrictions on deep types inside SPARK semantic checkings. (Is_Traversal_Function): Exported so that we can check for SPARK restrictions on traversal functions inside SPARK semantic checkings. (Check_Call_Statement, Read_Indexes): Check wether we are dealing with a subprogram pointer type before querying called entity. (Is_Subpath_Expression): Image attribute can appear inside a path. (Check_Loop_Statement): Correct order of statements in the loop. (Check_Node): Ignore raise nodes. (Check_Statement): Use Last_Non_Pragma to get the object declaration in an extended return statement.

1e5359c003a [Ada] Refactor ownership pointer checking in SPARK as a generic
gcc/ada/ChangeLog | 35 +++++
gcc/ada/gnat1drv.adb | 8 -
gcc/ada/sem_spark.adb | 413 +++++++++++++++++++++++++++++++++-----------------
gcc/ada/sem_spark.ads | 22 +++
4 files changed, 329 insertions(+), 149 deletions(-)

Upstream: gcc.gnu.org


  • Share