******************************************************* 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--------------------------------------------------