This patch provides the initial implementation of aspect Abstract_State. This construct is intended for formal verification proofs. The syntax of the aspect is as follows: abstract_state_list ::= null | state_name_with_properties | (state_name_with_properties { , state_name_with_properties } ) state_name_with_properties ::= state_name | ( state_name with property_list ) property_list ::= property { , property } property ::= simple_property | name_value_property simple_property ::= identifier name_value_property ::= identifier => expression state_name ::= defining_identifier The semantics of the aspect are as follows: The identifier of a simple_property shall be Volatile, Input, or Output. There shall be at most one occurrence of the identifiers Volatile, Input and Output in a single property_list. If a property_list includes Volatile, then it shall also include exactly one of Input or Output. If a property_list includes either Input or Output, then it shall also include Volatile. The identifier of a name_value_property shall be Integrity. If a property_list includes Integrity then it shall be the final property in the list. Each state_name occurring in an Abstract_State aspect specification for a given package P introduces an implicit declaration of a state abstraction entity. This implicit declaration occurs at the beginning of the visible part of P. This implicit declaration requires completion. A state abstraction shall only be named in contexts where this is explicitly permitted (e.g., as part of a Globals aspect specification), but this is not a name resolution rule. Thus, the declaration of a state abstraction has the same visibility as any other declaration. A state abstraction is not an object; it does not have a type. The completion of a state abstraction declared in a package aspect_specification can only be provided as part of a Refined_State aspect specification within the body of the package. A null abstract_state_list specifies that a package contains no hidden state or variables declared in its visible_part. A variable declared in the visible_part of a package implicitly declares a state abstraction entity with the same identifier as the defining_identifier of the variable. The variable declaration acts as the completion of the state abstraction. The implicitly declared state abstraction is only visible in a limited view of the package. A volatile state abstraction is one declared with a property list which includes the Volatile property, and either Input or Output. A Volatile Input or Output state abstraction represents a sequence of state changes brought about by reading or writing successive values to or from a volatile variable. ------------ -- Source -- ------------ -- semantics.ads package Semantics is package OK_1 with Abstract_State => null is end OK_1; package OK_2 with Abstract_State => (S_1, (S_2 with Volatile, Input, Integrity => 1), (S_3 with Output, Volatile, Integrity => 2)) is end OK_2; package Error_1 with Abstract_State => (S_1, S_1, -- duplicate state name 123, -- junk state name (123 with Input, Volatile), -- junk state name (S_2 with Junk_Name), -- junk property (S_3 with Input, Input), -- duplicate property (S_4 with Input), -- no Volatile (S_5 with Output), -- no Volatile (S_6 with Volatile), -- neither Input nor Output (S_7 with Volatile, Input, Output), -- can't have Input and Output (S_8 with Integrity => Junk_Value), -- has to be integer literal null) -- can't have null or any of the above is end Error_1; end Semantics; ----------------- -- Compilation -- ----------------- $ gcc -c -gnatc -gnat12 -gnatd.V semantics.ads semantics.ads:14:11: malformed abstract state declaration semantics.ads:16:09: "S_1" conflicts with declaration at line 15 semantics.ads:18:09: state name must be an identifier semantics.ads:19:18: invalid state property semantics.ads:20:25: duplicate state property semantics.ads:21:08: properties Input and Output require Volatile semantics.ads:22:08: properties Input and Output require Volatile semantics.ads:23:08: property Volatile requires exactly one Input or Output semantics.ads:24:08: property Volatile requires exactly one Input or Output semantics.ads:25:31: integrity level must be an integer literal semantics.ads:26:08: package "Error_1" has non-null abstract state Tested on x86_64-pc-linux-gnu, committed on trunk 2013-01-03 Hristian Kirtchev * aspects.adb, aspects.ads: Add Aspect_Abstract_State to all the relevant tables. * einfo.ads, einfo.adb: Add Integrity_Level and Refined_State to the description of fields (Abstract_States): New routine. (Integrity_Level): New routine. (Has_Property): New routine. (Is_Input_State): New routine. (Is_Null_State): New routine. (Is_Output_State): New routine. (Is_Volatile_State): New routine. (Refined_State): New routine. (Set_Abstract_States): New routine. (Set_Integrity_Level): New routine. (Set_Refined_State): New routine. (Write_Field8_Name): Add proper output for E_Abstract_State. (Write_Field9_Name): Add proper output for E_Abstract_State. (Write_Field25_Name): Add proper output for E_Package. * lib-xref.ads: Add new letter for an abstract state. * par-prag.adb: Add pragma Abstract_State to the list of pragma that do not need special processing by the parser. * sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect Abstract_State into a pragma without any form of legality checks. The work is done by Analyze_Pragma. (Check_Aspect_At_Freeze_Point): Aspect Abstract_State does not require delayed analysis. * sem_prag.adb: Add a value for pragma Abstract_State in table Sig_Flags. (Analyze_Pragma): Add legality checks for pragma Abstract_State. Analysis of individual states introduces a state abstraction entity into the visibility chain. * snames.ads-tmpl: Add new names for abstract state and integrity. Add new pragma id for abstract state.