******************************************************* Report of SPARK Examination SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 28-FEB-2010 12:06:46.11 Options: noindex_file nowarning_file notarget_compiler_data noconfig_file source_extension=ada listing_extension=lst nodictionary report_file=rep.rep html nostatistics fdl_identifiers flow_analysis=information ada95 annotation_character=# profile=sequential rules=none error_explanations=every_occurrence Selected files: @I:\SPARKworkspace\RandomNumbers\ND_Main.smf No Index files were used Meta File(s) used were: I:\SPARKworkspace\RandomNumbers\ND_Main.smf I:\SPARKworkspace\RandomNumbers\ND_RandomNumbers.ads I:\SPARKworkspace\RandomNumbers\spark_io.ads I:\SPARKworkspace\RandomNumbers\spark_io.adb I:\SPARKworkspace\RandomNumbers\MyIO.ads I:\SPARKworkspace\RandomNumbers\ND_Main.adb Full warning reporting selected Source Filename(s) used were: I:\SPARKworkspace\RandomNumbers\ND_RandomNumbers.ads [View analysis] I:\SPARKworkspace\RandomNumbers\spark_io.ads [View analysis] I:\SPARKworkspace\RandomNumbers\spark_io.adb [View analysis] I:\SPARKworkspace\RandomNumbers\MyIO.ads [View analysis] I:\SPARKworkspace\RandomNumbers\ND_Main.adb [View analysis] Source Filename: I:\SPARKworkspace\RandomNumbers\ND_RandomNumbers.ads Listing Filename: I:\SPARKworkspace\RandomNumbers\ND_RandomNumbers.lst [View HTML] Unit name: ND_RandomNumbers Unit type: package specification Unit has been analysed, any errors are listed below. No errors found Source Filename: I:\SPARKworkspace\RandomNumbers\spark_io.ads Listing Filename: I:\SPARKworkspace\RandomNumbers\spark_io.lst [View HTML] Unit name: Spark_IO Unit type: package specification Unit has been analysed, any errors are listed below. 29 error(s) or warning(s) Line 29 with Ada.Text_IO; ^1 --- ( 1) Warning : 1: The identifier Ada is either undeclared or not visible at this point. 66 --# declare delay; ^2 --- ( 2) Warning : 4: declare annotation - ignored by the SPARK Examiner. 78 --# declare delay; ^3 --- ( 3) Warning : 4: declare annotation - ignored by the SPARK Examiner. 85 --# declare delay; ^4 --- ( 4) Warning : 4: declare annotation - ignored by the SPARK Examiner. 92 --# declare delay; ^5 --- ( 5) Warning : 4: declare annotation - ignored by the SPARK Examiner. 99 --# declare delay; ^6 --- ( 6) Warning : 4: declare annotation - ignored by the SPARK Examiner. 114 --# declare delay; ^7 --- ( 7) Warning : 4: declare annotation - ignored by the SPARK Examiner. 121 --# declare delay; ^8 --- ( 8) Warning : 4: declare annotation - ignored by the SPARK Examiner. 152 --# declare delay; ^9 --- ( 9) Warning : 4: declare annotation - ignored by the SPARK Examiner. 158 --# declare delay; ^10 --- ( 10) Warning : 4: declare annotation - ignored by the SPARK Examiner. 163 --# declare delay; ^11 --- ( 11) Warning : 4: declare annotation - ignored by the SPARK Examiner. 179 --# declare delay; ^12 --- ( 12) Warning : 4: declare annotation - ignored by the SPARK Examiner. 186 --# declare delay; ^13 --- ( 13) Warning : 4: declare annotation - ignored by the SPARK Examiner. 225 --# declare delay; ^14 --- ( 14) Warning : 4: declare annotation - ignored by the SPARK Examiner. 231 --# declare delay; ^15 --- ( 15) Warning : 4: declare annotation - ignored by the SPARK Examiner. 241 --# declare delay; ^16 --- ( 16) Warning : 4: declare annotation - ignored by the SPARK Examiner. 258 --# declare delay; ^17 --- ( 17) Warning : 4: declare annotation - ignored by the SPARK Examiner. 265 --# declare delay; ^18 --- ( 18) Warning : 4: declare annotation - ignored by the SPARK Examiner. 274 --# declare delay; ^19 --- ( 19) Warning : 4: declare annotation - ignored by the SPARK Examiner. 281 --# declare delay; ^20 --- ( 20) Warning : 4: declare annotation - ignored by the SPARK Examiner. 299 --# declare delay; ^21 --- ( 21) Warning : 4: declare annotation - ignored by the SPARK Examiner. 307 --# declare delay; ^22 --- ( 22) Warning : 4: declare annotation - ignored by the SPARK Examiner. 315 --# declare delay; ^23 --- ( 23) Warning : 4: declare annotation - ignored by the SPARK Examiner. 322 --# declare delay; ^24 --- ( 24) Warning : 4: declare annotation - ignored by the SPARK Examiner. 340 --# declare delay; ^25 --- ( 25) Warning : 4: declare annotation - ignored by the SPARK Examiner. 349 --# declare delay; ^26 --- ( 26) Warning : 4: declare annotation - ignored by the SPARK Examiner. 357 --# declare delay; ^27 --- ( 27) Warning : 4: declare annotation - ignored by the SPARK Examiner. 365 --# declare delay; ^28 --- ( 28) Warning : 4: declare annotation - ignored by the SPARK Examiner. 386 end Spark_IO; --- ( 29) Warning : 10: The private part of package Spark_IO is hidden - hidden text is ignored by the SPARK Examiner. Source Filename: I:\SPARKworkspace\RandomNumbers\spark_io.adb Listing Filename: I:\SPARKworkspace\RandomNumbers\spark_io.lst [View HTML] Unit name: Spark_IO Unit type: package body Unit has been analysed, any errors are listed below. 1 error(s) or warning(s) Line 672 end Spark_IO; --- ( 1) Warning : 10: The body of package Spark_IO is hidden - hidden text is ignored by the SPARK Examiner. Source Filename: I:\SPARKworkspace\RandomNumbers\MyIO.ads Listing Filename: I:\SPARKworkspace\RandomNumbers\MyIO.lst [View HTML] Unit name: MyIO Unit type: package specification Unit has been analysed, any errors are listed below. No errors found Source Filename: I:\SPARKworkspace\RandomNumbers\ND_Main.adb Listing Filename: I:\SPARKworkspace\RandomNumbers\ND_Main.lst [View HTML] Unit name: Main Unit type: main program Unit has been analysed, any errors are listed below. No errors found --End of file--------------------------------------------------