CVS difference for ai12s/ai12-0254-1.txt

Differences between 1.3 and version 1.4
Log of other versions for file ai12s/ai12-0254-1.txt

--- ai12s/ai12-0254-1.txt	2018/03/02 06:46:46	1.3
+++ ai12s/ai12-0254-1.txt	2018/03/06 23:36:05	1.4
@@ -1,15 +1,17 @@
-!standard A.18.32(0)                                  18-01-31  AI12-0254-1/02
+!standard A.18.32(0)                                  18-03-06  AI12-0254-1/03
 !class Amendment 18-01-26
+!status Amendment 1-2012 18-03-05
+!status ARG Approved 7-1-4  18-03-05
 !status work item 18-01-26
 !status received 18-01-15
-!priority Very_Low
+!priority Low
 !difficulty Easy
 !subject Bounded_Indefinite_Holders
 !summary
 
 The Bounded_Indefinite_Holder container is added to allow the use of
 class-wide objects in safety critical environments where dynamic allocation
-are not allowed.
+is not allowed.
 
 !problem
 
@@ -23,18 +25,18 @@
 On the other hand, it is desirable, and becoming accepted, to use tagged
 types and dynamic dispatching even in high-integrity applications.
 Static analysis tools for stack usage can usually deal with the dynamic
-dispatching (even if it introduces some over-estimation), but a harder
+dispatching (even if it introduces some overestimation), but a harder
 problem is that dynamic dispatching requires class-wide subtypes, which
 are currently considered indefinite subtypes by RM3.3(23/3) and for
 which the compiler cannot know the size, at compile time, from local
 analysis of the program. The amount of memory consumed by an object of a
-class-wide subtype is therefore defined at run-time, in practice by
+class-wide subtype is therefore defined at runtime, in practice by
 using heap or secondary stack (or some way of extending the local stack
 frame of the primary stack, equally difficult for static stack-usage
 analysis).
 
 Moreover, the indefiniteness of class-wide types means that data
-structures (array, records, etc.) with components of class-wide type can
+structures (arrays, records, etc.) with components of class-wide type can
 be created only by using heap allocation and access-to-class-wide
 components. But in high-integrity applications, heap use is often
 completely forbidden.
@@ -71,11 +73,11 @@
 Containers.Bounded_Indefinite_Holders has the same contents and semantics as
 Containers.Indefinite_Holders except:
 
-* "with System.Storage_Elements; use System.Storage_Elements;" is added to
-   the context clause;
+* The following is added to the context clause:
+     with System.Storage_Elements; use System.Storage_Elements;
 
 * An additional generic parameter follows Element_Type:
-     Max_Element_Size_in_Storage_Elements : Storage_Elements.Storage_Count;
+     Max_Element_Size_in_Storage_Elements : Storage_Count;
 
   AARM Reason: This value is in Storage_Elements so that it can be used as a
   discriminant on a storage pool object in the implementation of the object;
@@ -88,31 +90,15 @@
   End AARM Reason.
 
 * Add to the precondition of To_Holder and Replace_Element:
-     and (if New_Item'Size <=
-             Max_Element_Size_in_Storage_Elements * System.Storage_Unit
-          then (raise Program_Error))
+     and then (if New_Item'Size >
+                  Max_Element_Size_in_Storage_Elements * System.Storage_Unit
+               then raise Program_Error)
 
   AARM Reason: This ensures that an object that won't fit is not inserted into
   the container.
 
 Bounded (Run-time) Errors
 
-It is a bounded error call To_Holder or Replace_Element on a bounded holder if
-the New_Item object would require more than one call to Allocate of a storage
-pool (see 13.11). Either Program_Error is raised by the operation, or execution
-proceeds normally. 
-
-  AARM Reason: Implementation of this container in Ada will probably
-  require the use of a special storage pool which only allows a single
-  allocation. If putting the New_Item object into the holder requires multiple
-  calls to Allocate, we allow raising Program_Error rather than requiring a
-  complex storage pool implementation that would effectively be the same as the
-  dynamic allocation that we are trying to avoid.
-
-  AARM Discussion: Whether this happens for a particular type depends on the
-  implementation. Formally, how many calls to Allocate are required is
-  unspecified; hopefully the implementation will document this anyway.
-
 It is a bounded error to assign from a bounded holder object while tampering
 with elements of that object is prohibited. Either Program_Error is raised by
 the assignment, execution proceeds with the target object prohibiting tampering
@@ -120,7 +106,7 @@
 
 Implementation Requirements
 
-For each instance of Containers.Indefinite__Holders and each instance of
+For each instance of Containers.Indefinite_Holders and each instance of
 Containers.Bounded_Indefinite_Holders, if the two instances meet the following
 conditions, then the output generated by the Holder'Output or Holder'Write
 subprograms of either instance shall be readable by the Holder'Input or
@@ -145,20 +131,29 @@
 procedures). All storage pools are controlled, so we can't reasonably say
 that a bounded holder will not need finalization.
 
+AARM Implementation Note: If the implementation supports discontiguous objects
+that require multiple calls to Allocate in a storage pool, the storage pool
+will need to support such allocations. The storage pool implementation can
+assume that all Allocate calls occur together, and similarly for Deallocate
+calls, thus simplifying the pool implementation so that allocation only occurs
+at a high-water mark location.
+
+
 !discussion
 
 This container can be used to solve the Problem by putting the class-wide
-objects into holders. Assuming that they fit and are allocated contiguously,
-the holder can be used like any other fixed-size object.
+objects into holders. Assuming that they fit, the holder can be used like any
+other fixed-size object.
 
 Thoughts:
 
 [1] The Bounded_Indefinite_Holder could be implemented in Ada using a storage
 pool that has a discriminant of the size of the data area required. Then,
-allocation/decallocation of a single object would be supported. This code would
-be very simple (simply directly returning an address from allocate and setting
-a Boolean to indicate that allocation has happened) and could easily be
-analyzed if needed.
+allocation/deallocation of a single object would be supported. If the all data
+types are allocated contiguously (common in compilers targeting applications
+that cannot allow heap use), this code would be very simple (simply directly
+returning an address from allocate and setting a Boolean to indicate that
+allocation has happened) and could easily be analyzed if needed.
 
 Such a storage pool would require finalization, but the actual finalize routine
 could be a null procedure. An Ada compiler targeting these sorts of
@@ -205,15 +200,72 @@
 size), this would result in the preconditions being known to pass (and thus not
 generating any code). Such an optimization would probably take some extra
 implementation work (it wouldn't fall out naturally like (1)), but it could
-be implemented for a compiler targetting this sort of application.
+be implemented for a compiler targeting this sort of application.
 
 (3) This issue also could be handled with a technique recommended by AdaCore
 for such systems: use a tool like SPARK to prove that the checks cannot fail,
-then suppress them. Precondition checks on language-defined units can be
-suppressed (using a suppress mechanism defined in AI12-0112-1), and thus
-not appear in the generated code. If the correctness has been verified some
-other way, this will not cause any safety issues.
+then suppress them. Precondition checks on language-defined container units
+can be suppressed (using a suppress mechanism defined in AI12-0112-1), and
+thus not appear in the generated code. If the correctness has been verified
+some other way, this will not cause any safety issues.
+
+!corrigendum A.18.32(0)
+
+@dinsc
+
+The language-defined generic package Containers.Bounded_Indefinite_Holders
+provides a private type Holder and a set of operations for that type. It
+provides the same operations as the package Containers.Indefinite_Holders
+(see A.18.18), with the difference that the maximum storage is bounded.
+
+@s8<@i<Static Semantics>>
+
+The declaration of the generic library package
+Containers.Bounded_Indefinite_Holders has the same contents and semantics as
+Containers.Indefinite_Holders except:
+
+@xbullet<The following is added to the context clause:>
+
+@xcode<   @b<with> System.Storage_Elements; @b<use> System.Storage_Elements;>
+@xbullet<An additional generic parameter follows Element_Type:>
+
+@xcode<   Max_Element_Size_in_Storage_Elements : Storage_Elements.Storage_Count;>
 
+@xbullet<Add to the precondition of To_Holder and Replace_Element:>
+
+@xcode<   @b<and then> (@b<if> New_Item'Size @>
+                Max_Element_Size_in_Storage_Elements * System.Storage_Unit
+             @b<then raise> Program_Error)>
+
+@s8<@i<Bounded (Run-time) Errors>>
+
+It is a bounded error to assign from a bounded holder object while tampering
+with elements of that object is prohibited. Either Program_Error is raised by
+the assignment, execution proceeds with the target object prohibiting tampering
+with elements, or execution proceeds normally. 
+
+@s8<@i<Implementation Requirements>>
+
+For each instance of Containers.Indefinite_Holders and each instance of
+Containers.Bounded_Indefinite_Holders, if the two instances meet the following
+conditions, then the output generated by the Holder'Output or Holder'Write
+subprograms of either instance shall be readable by the Holder'Input or
+Holder'Read of the other instance, respectively:
+
+@xbullet<the Element_Type parameters of the two instances are statically
+matching subtypes of the same type; and>
+
+@xbullet<the output generated by Element_Type'Output or Element_Type'Write is
+readable by Element_Type'Input or Element_Type'Read, respectively
+(where Element_Type denotes the type of the two actual Element_Type
+parameters).>
+
+@s8<@i<Implementation Advice>>
+
+Bounded holder objects should be implemented without dynamic allocation and
+any finalization should be trivial unless Element_Type needs finalization. 
+
+
 !ASIS
 
 No changes needed for package Bounded_Indefinite_Holders.
@@ -671,7 +723,7 @@
 
 ****************************************************************
 
-From: Niklas Holsti
+From: Randy Brukardt
 Sent: Monday, January 22, 2018  3:16 PM
 
 > I'm afraid that is not true for static analysis of resource usage,

Questions? Ask the ACAA Technical Agent