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