*******************************************************
                           Listing of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06
                           Demonstration Version
          *******************************************************


                       DATE : 28-FEB-2010 12:47:10.00

Line
   1  --# main_program;
   2  procedure Main
   3  --# derives ;
   4  is
   5    G : Integer;
   6  --
   7    function F1(I: in Integer) return Integer
   8    --# global G;
   9    is begin
  10      return I;
  11    end F1;

!!! (  1)  Flow Error        : 30: The variable G is imported but neither 
           referenced nor exported.
!!! (  2)  Flow Error        : 50: The function value is not derived from the 
           imported value(s) of G [Explanatory note: The item before "is not 
           derived ..." is an export or function return value and the item(s) 
           after are imports of the subprogram.  The message indicates that a 
           dependency, stated in the dependency relation (derives annotation) 
           or implied by the function signature is not present in the code. The 
           absence of a stated dependency is always an error in either code or 
           annotation.].

  12  --
  13    function Random return Integer
  14    --# global G;
  15    is begin
  16      return G**2;
  17    end Random;

+++        Flow analysis of subprogram Random performed: no 
           errors found.

  18  
  19  
  20  begin
  21    null;
  22  end Main;

--- (  3)  Warning           :400: Variable G is declared but not used [Explanatory 
           note: Issued when a variable declared in a subprogram is neither 
           referenced, nor updated. (warning control file keyword: 
           unused_variables)].
+++        Flow analysis of subprogram Main performed: no 
           errors found.



--End of file--------------------------------------------------