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


                       DATE : 19-FEB-2010 10:53:12.51

Line
   1  package body RandomNumbers is
   2     State : Integer;
   3     procedure Random(X : out Float) is
   4     -- --# hide Random
   5     begin
   6        X:=Float(State+1); -- just to do something
   7        State:=State*2;
   8     end Random;

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

   9  begin
  10     State := 2**15 - 1;
  11  end RandomNumbers;

+++        Flow analysis of package initialization 
           performed: no errors found.



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