diff options
Diffstat (limited to 'gcc/ada/exp_spark.ads')
| -rw-r--r-- | gcc/ada/exp_spark.ads | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads index 726b69ac014..c422bc73e52 100644 --- a/gcc/ada/exp_spark.ads +++ b/gcc/ada/exp_spark.ads @@ -30,54 +30,6 @@ -- Expand_SPARK is called directly by Expander.Expand. --- SPARK expansion has three main objectives: - --- 1. Perform limited expansion to explicit some Ada rules and constructs --- (translate 'Old and 'Result, replace renamings by renamed, insert --- conversions, expand actuals in calls to introduce temporaries, expand --- generics instantiations) - --- 2. Facilitate treatment for the formal verification back-end (fully --- qualify names, expand set membership, compute data dependences) - --- 3. Avoid the introduction of low-level code that is difficult to analyze --- formally, as typically done in the full expansion for high-level --- constructs (tasking, dispatching) - --- To fulfill objective 1, Expand_SPARK selectively expands some constructs. - --- To fulfill objective 2, the tree after SPARK expansion should be fully --- analyzed semantically. In particular, all expression must have their proper --- type, and semantic links should be set between tree nodes (partial to full --- view, etc.) Some kinds of nodes should be either absent, or can be ignored --- by the formal verification backend: - --- N_Object_Renaming_Declaration: can be ignored safely --- N_Expression_Function: absent (rewitten) --- N_Expression_With_Actions: absent (not generated) - --- SPARK cross-references are generated from the regular cross-references --- (used for browsing and code understanding) and additional references --- collected during semantic analysis, in particular on all --- dereferences. These SPARK cross-references are output in a separate section --- of ALI files, as described in spark_xrefs.adb. They are the basis for the --- computation of data dependences in the formal verification backend. This --- implies that all cross-references should be generated in this mode, even --- those that would not make sense from a user point-of-view, and that --- cross-references that do not lead to data dependences for subprograms can --- be safely ignored. - --- To support the formal verification of units parameterized by data, the --- value of deferred constants should not be considered as a compile-time --- constant at program locations where the full view is not visible. - --- To fulfill objective 3, Expand_SPARK does not expand features that are not --- formally analyzed (tasking), or for which formal analysis relies on the --- source level representation (dispatching, aspects, pragmas). However, these --- should be semantically analyzed, which sometimes requires the insertion of --- semantic pre-analysis, for example for subprogram contracts and pragma --- check/assert. - with Types; use Types; package Exp_SPARK is |