This patch corrects the insertion of the corresponding pragma for aspect
Abstract_State when the related construct is a nested package. The pragma
appears in the visible declarations of the package.
-- Source --
-- pack.ads
package Pack with Abstract_State => Pack_Stat
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
