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


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

Line
   1  --# main_program;
   2  procedure Main
   3  --# derives ;
   4  is
   5    procedure AC1(X : in out Float; I: in Integer; 
   6  			     M : out Boolean )
   7    --# derives X from *, I & M from I;
   8    is begin
   9      M := True;
  10    end AC1;

!!! (  1)  Flow Error        : 35: Importation of the initial value of variable X 
           is ineffective [Explanatory note: The meaning of this message is 
           explained in Section 4.2 of Appendix A].
!!! (  2)  Flow Error        : 31: The variable X is exported but not (internally) 
           defined.
!!! (  3)  Flow Error        : 30: The variable I is imported but neither 
           referenced nor exported.
!!! (  4)  Flow Error        : 50: X is not derived from the imported value(s) of X, 
           I [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.].

!!! (  5)  Flow Error        : 50: M is not derived from the imported value(s) of I 
           [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.].

  11  --
  12    procedure AC2(X : in out Float; I: in Integer; 
  13  			     M : out Boolean )
  14    --# derives X from *, I & M from I;
  15    is 
  16    begin
  17      M := I mod 2 = 0;
  18    end AC2;

!!! (  6)  Flow Error        : 35: Importation of the initial value of variable X 
           is ineffective [Explanatory note: The meaning of this message is 
           explained in Section 4.2 of Appendix A].
!!! (  7)  Flow Error        : 31: The variable X is exported but not (internally) 
           defined.
!!! (  8)  Flow Error        : 50: X is not derived from the imported value(s) of X, 
           I [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.].

  19  --
  20    procedure AC3(X : in out Float; I: in Integer; 
  21  			     M : out Boolean )
  22    --# derives X from *, I & M from I;
  23    is 
  24    begin
  25      M := I mod 2 = 0;
  26      if M then
  27  	X:= 2**I; -- conversione implicita
  28      end if;
  29    end AC3;

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

  30  --
  31    procedure AC4(X : out Float; I: in Integer; 
  32  			     M : out Boolean )
  33    --# derives X from *, I & M from I;
                           ^9
*** (  9)  Semantic Error    :162: Importation of X is incompatible with its 
           parameter mode [Explanatory note: Issued if a parameter appears as 
           an import to a procedure when it is of parameter mode out.].

  34    is 
  35    begin
  36      M := I mod 2 = 0;
  37      if M then
  38  	X:= 2**I; -- conversione implicita
  39      end if;
  40    end AC4;
  41  --
  42    procedure AC5(X : out Float; I: in Integer; 
  43  			     M : out Boolean )
  44    --# derives X,M from I;
  45    is 
  46    begin
  47      M := I mod 2 = 0;
  48      if M then
  49  	X:= 2**I; -- conversione implicita
  50      end if;
  51    end AC5;

??? ( 10)  Warning           :602: The undefined initial value of X may be used in 
           the derivation of X [Explanatory note: Here XXX is a non-imported 
           variable, and YYY is an export, of a procedure subprogram.].

  52  --
  53    procedure AC6(X : out Float; I: in Integer; 
  54  			     M : out Boolean )
  55    --# derives X,M from I;
  56    is 
  57    begin
  58      M := I mod 2 = 0;
  59      if M then
  60  	X:= 2**I; -- conversione implicita
  61      else
  62       X := 0.0;
  63      end if;
  64    end AC6;

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

  65  --
  66    procedure AC7(X : out Float; I: in Integer; 
  67  			     M : out Boolean )
  68    --# derives X,M from I;
  69    is 
  70    begin
  71      M := I mod 2 = 0;
  72      if M then
  73  	X:= 1.0;
  74      else
  75       X := 0.0;
  76      end if;
  77    end AC7;

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

  78  
  79  begin
  80    null;
  81  end Main;

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



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