This is only an initial implementation, subject to many limitations. Some interactions with derived types and inheritance are not implemented. Other limitations are idenitified in the code with "???" comments. However, Stable_Properties and Stable_Properties'Class aspect specifications are implemented for both types and subprograms and the associated assertions are generated.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* snames.ads-tmpl: Define new Name_Stable_Properties Name_Id
value.
* aspects.ads, aspects.adb: Add new Aspect_Stable_Properties
enumeration literal to Aspect_Id type. Add Class_Present
parameter to Find_Aspect and related
functions (Find_Value_Of_Aspect and Has_Aspect).
* sem_util.adb (Has_Nontrivial_Precondition): Fix
previously-latent bug uncovered by adding Class_Present
parameter to Aspect.Find_Aspect. The code was wrong before, but
with the change the bug was more likely to make a user-visible
difference.
* sem_ch6.adb (Analyze_Operator_Symbol): If a string literal
like "abs" or "-" occurs in a Stable_Properties aspect
specification, then it is to be interpreted as an operator
symbol and not as a string literal.
* sem_ch13.ads: Export new Parse_Aspect_Stable_Properties
function, analogous to the existing Parse_Aspect_Aggregate
exported procedure.
* sem_ch13.adb: (Parse_Aspect_Stable_Properties): New function;
analogous to existing Parse_Aspect_Aggregate.
(Validate_Aspect_Stable_Properties): New procedure; analogous to
existing Validate_Aspect_Aggregate. Called from the same case
statement (casing on an Aspect_Id value) where
Validate_Aspect_Aggregate is called.
(Resolve_Aspect_Stable_Properties): New procedure; analogous to
existing Resolve_Aspect_Aggregate. Called from the same two case
statements (each casing on an Aspect_Id value) where
Resolve_Aspect_Aggregate is called.
(Analyze_Aspect_Specifications): Set Has_Delayed_Aspects and
Is_Delayed_Aspect attributes for Aspect_Stable_Properties aspect
specifications.
(Check_Aspect_At_End_Of_Declarations): The syntactic
"expression" for a Stable_Properties aspect specification is not
semantically an expression; it doesn't have a type. Thus, force
T to be empty in this case.
* contracts.adb (Expand_Subprogram_Contract): Add call to new
local procedure,
Expand_Subprogram_Contract.Add_Stable_Property_Contracts, which
generates Postcondition pragmas corresponding to stable property
checks.
patch.diff.gz
Description: application/gzip
