CVS difference for ai12s/ai12-0079-1.txt
--- ai12s/ai12-0079-1.txt 2018/11/13 05:47:38 1.21
+++ ai12s/ai12-0079-1.txt 2018/11/15 21:26:26 1.22
@@ -1,4 +1,4 @@
-!standard 6.1.2(0) 18-10-19 AI12-0079-1/08
+!standard 6.1.2(0) 18-10-21 AI12-0079-1/09
!class Amendment 13-06-28
!status work item 13-06-28
!status received 13-06-14
@@ -85,17 +85,6 @@
[for all X convertible to A => X.all]
-Also allow within a Global or Global'Class aspect
-a reference to the set of pointed-to objects reachable from
-a given object (of an access type or a composite type) using the attribute
-P'Reachable. This attribute can also be used as a predicate to check
-for overlap between the reachable object set and specific objects or
-with another reachable object set, such as "P'Reachable(Obj1, Obj2)" or
-"not P'Reachable(Q'Reachable)." Also can use this in a postcondition
-to specify when new objects are added or removed from the Reachable set
-(to add: "P'Reachable(Q'Reachable'Old)"; to remove: "not P'Reachable(Obj2)";
-to remove all: "P'Reachable = (<>)").
2. Allow the name of a package P to stand-in for the set of objects
described roughly by:
@@ -134,43 +123,6 @@
-Add after 6.1.1(30.3/5) -- at the end of static semantics:
- Given an access-to-object type T that has Ownership aspect False (see
- H.7), an aliased object is /reachable/ from an access object X of type
- T if the aliased object satisfies the constraints of the designated
- subtype of T and any constraints that apply to X, and, when T is a
- pool-specific access type, the aliased object might be part of the
- collection (see 7.6.1) associated with T. In addition, an aliased
- object is reachable from X if it is reachable from a part of an object
- that is itself reachable from X. Reachability from access objects of a
- type with Ownership aspect True is defined in H.7. An aliased object is
- /reachable/ from a composite object if the aliased object is reachable
- from some subcomponent of the composite object.
- AARM Reason: Reachability is defined in terms of types rather than
- individual objects, in the absence of "ownership." See H.7 (AI-0240)
- for the rules that apply when ownership is True.
- AARM Ramification: This notion of reachability is very imprecise,
- and so it is not particularly useful for identifying true data
- races. It avoids having to expose particular access types used to
- represent parts of private types, as X'Reachable essentially
- represents the set of access types used in the representation of X,
- without having to name them. Some notion of ownership, as proposed
- in AI12-0240, seems essential to identify true data races in the
- presence of access types.
- Within the aspect specification for a Post or Post'Class aspect, the
- following attribute function is defined for an object X of an access
- or composite type, where global_set is as defined in 6.1.2:
- X'Reachable (global_set)
- X'Reachable (global_set) returns True if at least one object in the set
- identified by the global_set is reachable from X.
- AARM Rationale: This allows a postcondition to indicate what additional
- objects might become reachable from X as a result of invoking the
Add the following section:
6.1.2 The Global and Global'Class Aspects
@@ -216,7 +168,6 @@
| /package_/name [ PRIVATE ]
| ACCESS subtype_mark
- | /object_/name'Reachable
A /global_/attribute_reference is an attribute_reference with attribute
@@ -323,10 +274,7 @@
can be designated by values of the given access-to-variable type;
* ACCESS subtype_mark identifies the set of (aliased) variables that
can be designated by values of an access-to-variable type with a
- designated subtype statically matching the given subtype_mark;
- * /object_/name'Reachable identifies the set of (aliased) variables
- that are reachable (see 6.1.1) from the object denoted by
+ designated subtype statically matching the given subtype_mark.
@@ -399,8 +347,7 @@
The intent is that all of the global in, in-out, and out annotations
-proposed can be statically checked. Those involving 'Reachable need further
-explanation -- see below for our discussion of 'Reachable.
+proposed can be statically checked.
We have allowed for an implementation-defined global_mode_qualifier, which
would allow "proof in" for SPARK, as well as something like "synthesized
@@ -415,20 +362,6 @@
check, but thankfully is covered by B.1(38.1/2). Incorrect annotations
on imported subprograms could cause a program's execution to be erroneous.
-We have defined a 'Reachable attribute which can be used in the presence
-of access types, either visibly or hidden within a private type, to
-indicate side-effects on directly or indirectly designated (aliased) objects.
-A corresponding attribute function 'Reachable(obj1, obj2, ...) can be used
-in postconditions to specify how the set of reachable objects is affected
-by a subprogram.
-To check the uses of X'Reachable within global aspect specifications, the
-compiler needs to verify that, for dereferences that are *not* covered by
-global_name's of the form "access T" or the name of an access type, they
-fall within some X'Reachable set. In the absence of pointer "ownership"
-(see AI12-0240), X'Reachable is defined in terms of what access *types*
-are "reachable" from X, so it should be checkable at compile time.
SPARK does not currently support identifying particular components of a
global variable in the Global aspect, but for Ada we plan to allow that.
This is somewhat inconsistent with what can be specified for parameters,
@@ -478,8 +411,7 @@
with Global => T'Global;
procedure Insert(S : in out Set; X : T)
- with Global => in out S'Reachable & Hash'Global & T'Global,
- Post => S'Reachable(X'Copy'Reachable);
+ with Global => in out Hash'Global & T'Global;
@@ -489,12 +421,6 @@
Hash, and as a result of dereferencing access objects within the
representation of a Set. The default initialization, adjustment, and
finalization of a Set indirectly uses the corresponding operations of T.
-Insert updates the objects reachable from S, as well as those updated
-by Hash and T's assignment operation, and has a post-condition that
-indicates it makes the objects reachable from X'Copy reachable from S
-(in addition to those originally reachable from S). X'Copy is used here
-to indicate that we are not using X directly, but rather copying X
-into the data structure that represents S.
Questions? Ask the ACAA Technical Agent