CVS difference for ais/ai-00209.txt

Differences between 1.3 and version 1.4
Log of other versions for file ais/ai-00209.txt

--- ais/ai-00209.txt	1999/02/28 01:43:03	1.3
+++ ais/ai-00209.txt	2000/11/28 23:48:47	1.4
@@ -1,4 +1,4 @@
-!standard H.3.1     (8)                             99-02-05  AI95-00209/01
+!standard H.3.1     (8)                             00-11-13  AI95-00209/02
 !class binding interpretation 99-02-05
 !status work item 99-02-05
 !status received 98-10-01
@@ -6,105 +6,126 @@
 !difficulty Easy
 !subject pragma Reviewable; can objects become uninitialized?
 
-!summary 99-02-05
+!summary
 
 In H.3.1(8), the term "reference (to)" needs to be replaced by "usage
-(of the value of)".
+(of the value of)". H.3.2(9) needs to be similarly changed.
 
 For the purposes of Pragma Reviewable, objects are uninitialized, if
-they never were initialized or assigned to prior to use.  Objects
-cannot become uninitialized by assigning the value of an uninitialized
-object to them. Formal IN and IN OUT parameters are always considered
-initialized.
+they never were initialized or assigned to prior to use. All such
+objects must be identified by an implementation in conformance with
+H.3.1(8).
 
-An implementation may, but need not, take advantage of aliasing analysis in
-determining whether or not an object is initialized.
+An implementation may identify additional objects as uninitialized, if
+the value of an uninitialized object is assigned to them.
 
-!question 98-10-01
+An implementation may, but need not, take advantage of aliasing
+analysis or knowledge of non-executable program paths in determining
+whether or not an object is initialized.
 
-When pragma Reviewable is being used, can objects become uninitialized? [No.]
+!question
 
+When pragma Reviewable is being used, can objects become uninitialized?
+
 Consider the following example:
 
 declare
-   A : Integer := 42;  
+   A : Integer := 42;
    B : Integer;
    C : Integer;
 begin
    A := C;  -- C is uninitialized
-   B := A;  -- Is A initialized??? [Yes.]
+   B := A;  -- Is A initialized???
 end;
 
 The error in the program above is clearly the first statement.
-Will it be correct to state at the reference to C, that C is "possibly
-unititialized" and at the reference to A, that A is "known to be
+Will it be correct to state at the usage of C, that C is "possibly
+uninitialized" and at the subsequent usage of A, that A is "known to be
 initialized" (initialized once, always initialized)?
 
-!recommendation 99-02-05
+!recommendation
 
 (see summary)
 
-!wording 99-02-05
+!wording
 
 H.3.1(8) should read: "For each usage of the value of a scalar object,
 an identification of the usage as either ....."
+
+The 2. sentence of H.3.2(9) should read: "Thus an inspection point has
+the effect of an implicit usage of the value of each of its
+inspectable objects."
 
-!discussion 99-02-05
+!discussion
 
 First, the term "reference" in H.3.1(8) is incorrect as it also
 includes the occurrence as the target of an assignment. Clearly, only
-usages of the value of the object were meant to be diagnosed.
+usages of the value of the object were meant to be diagnosed. Similarly,
+the NOTE H.3.2(9) in imprecise by its usage of the term "reference".
 
-If assignments of uninitialized values to objects were to
-"deinitialize" their target objects, the benefits of the diagnostics
-would be lessened, since they would no longer distinguish between
-truly uninitialized objects and those that were transitively
-affected.
+A definitive answer to the !question seems counter-productive. A model
+that allows for a "deinitialization" caused by assigning the value of
+an uninitialized object may, at times, be beneficial to a programmer
+interested in knowing why an operation in the program causes a value
+failure of the software. This benefit cannot be obtained, if we
+restrict the model to a "once assigned, always initialized" model.
+
+On the other hand, the deinitialization model will be a significant
+nuisance during an overall examination of a program in search of any
+use of truly uninitialized objects. Here, the "once assigned, always
+initialized" model is preferable, since, after correction of any original
+uninitialized usages, the consequential "deinitializations" will have
+automatically disappeared.
 
 The main disadvantage arises, when an object remains "possibly
 uninitialized" only because the compiler is unable to prove the
-falsehood of the path predicate, on which the object would be
+falsehood of the path predicate, under which the object would be
 uninitialized. A user (or verification system) will then have to
 examine the code to establish that on all executable paths to the
 usage point the object is indeed initialized. Once this is
 established, clearly no other variable can be deinitialized by being
-assigned the object's value. However, if the compiler diagnostics need
-to assume transitive infection, then these other variables will
+assigned the object's value. However, if the compiler diagnostics
+assume transitive infection, then these other variables will
 (continue to) be diagnosed as uninitialized, misleading the user.
 Consider:
   if P then X := 7; end if;
   ...
-  if P then Y := X; end if;
-Of course, Y is well defined under all circumstances. However,
-the transitive infection model would make Y an uninitialized
-variable, since X is "potentially uninitialized" at this point.
-The fact that X is initialized depends on the branch
-predicates involved and is, in general, undecidable. Surely
-users will not want to laboriously determine that Y (and whatever
-it transitively affects) is diagnosed as "uninitialized" only
-because of the situation above.
-
-As a smaller issue, a transitive model would have to explain
-the difference between
-    A := C;
-and
-    A := C + 0;
-    A:= f(X); -- with f referencing C in its result computation
-Do the latter assignments also deinitialize if C is uninitialized ?
-
-We conclude that assignments by ininitialized objects should not
-deinitialize the target object.
+  if Q then Y := X; else Y := 6; end if;
+  A := Y;
+  B:= A + 1;
+
+Assume further that Q implies P. Of course, Y is then well defined
+under all circumstances. However, the transitive infection model would
+make Y, and consequently A and B, uninitialized variables, since X is
+"potentially uninitialized" at this point.  The fact that X is
+initialized depends on the branch predicates involved and is, in
+general, undecidable. Surely users will not want to laboriously
+determine that Y and whatever it transitively affects, i.e., the
+variables A and B, are diagnosed as "uninitialized" only
+because of such situations. The non-transitive model will correctly
+identify the usage of X as "potentially uninitialized" and thus
+identify the cause of a potential error, but leave Y, A, and B
+undiagnosed, since the problem is clearly not at the point of their
+usages.
+
+Given the two presented usage scenarios of the diagnostics, we do
+not want to favor one analysis model over the other. Rather, it is
+best left to the negotiations between vendors supporting this annex
+and their users, which of the models should be followed by the
+implementation.
 
 An object may be initialized through an aliasing effect. As aliasing
 analysis is rather difficult and, in general, undecidable, albeit not
 for scalar objects, Pragma Reviewable should not require the compiler
-to perform such an analysis. The effect on the diagnostics of uninitialized
-objects is conservatively correct, that is, all uninitialized objects
-will be recognized, but some objects initialized only by alias-effect
-will also be diagnosed as uninitialized.
+to perform such an analysis.
 
+In summary, the diagnostics of uninitialized objects must be
+conservatively correct, that is, all uninitialized objects will be
+recognized, but some objects initialized only by alias-effects or
+uninitialized only on non-executable paths, or assigned the value of
+an uninitialized object may also be diagnosed as uninitialized.
 
-!appendix 99-02-08
+!appendix
 
 !topic pragma Reviewable; "known to be inititialized"
 !reference AARM95-H.3.1(8);6.0
@@ -124,7 +145,7 @@
 Consider the following example:
 
 declare
-   A : Integer := 42;  
+   A : Integer := 42;
    B : Integer;
    C : Integer;
 begin

Questions? Ask the ACAA Technical Agent