******************************************************* Report of SPARK Examination SPARK Examiner GPL Edition, Version 8.1.1, Build Date 20090505, Build 13202 Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K. ******************************************************* DATE : 15-APR-2010 10:29:08.97 Options: noindex_file warning_file=J:\SPARKworkspace\TimeT\tis.wrn notarget_compiler_data noconfig_file source_extension=ada listing_extension=ls_ nodictionary report_file=rep.rep html exp_checks rtc vcs nostatistics fdl_identifiers flow_analysis=information ada95 annotation_character=# profile=sequential rules=none error_explanations=every_occurrence justification_option=full Selected files: @J:\SPARKworkspace\TimeT\clock.smf No Index files were used Meta File(s) used were: J:\SPARKworkspace\TimeT\clock.smf J:\SPARKworkspace\TimeT\basictypes.ads J:\SPARKworkspace\TimeT\time.ads J:\SPARKworkspace\TimeT\time.adb J:\SPARKworkspace\TimeT\time-interface.ads J:\SPARKworkspace\TimeT\time-interface.adb J:\SPARKworkspace\TimeT\clock.ads J:\SPARKworkspace\TimeT\clock.adb Summary warning reporting selected for: Hidden parts Representation clauses With clauses lacking a supporting inherit Uses of Ada2005 reserved words Notes Source Filename(s) used were: J:\SPARKworkspace\TimeT\basictypes.ads [View analysis] J:\SPARKworkspace\TimeT\time.ads [View analysis] J:\SPARKworkspace\TimeT\time.adb [View analysis] J:\SPARKworkspace\TimeT\time-interface.ads [View analysis] J:\SPARKworkspace\TimeT\time-interface.adb [View analysis] J:\SPARKworkspace\TimeT\clock.ads [View analysis] J:\SPARKworkspace\TimeT\clock.adb [View analysis] Source Filename: J:\SPARKworkspace\TimeT\basictypes.ads Listing Filename: J:\SPARKworkspace\TimeT\basictypes.lss [View HTML] Unit name: BasicTypes Unit type: package specification Unit has been analysed, any errors are listed below. No errors found 3 summarized warning(s), comprising: 3 representation clause(s)* (*Note: the above warnings may affect the validity of the analysis.) Source Filename: J:\SPARKworkspace\TimeT\time.ads Listing Filename: J:\SPARKworkspace\TimeT\time.lss [View HTML] Unit name: Time Unit type: package specification Unit has been analysed, any errors are listed below. No errors found No summarized warnings Source Filename: J:\SPARKworkspace\TimeT\time.adb Listing Filename: J:\SPARKworkspace\TimeT\time.lsb [View HTML] Unit name: Time Unit type: package body Unit has been analysed, any errors are listed below. No errors found No summarized warnings Source Filename: J:\SPARKworkspace\TimeT\time-interface.ads Listing Filename: J:\SPARKworkspace\TimeT\time-interface.lss [View HTML] Unit name: Time.Interface Unit type: package specification Unit has been analysed, any errors are listed below. No errors found 2 summarized warning(s), comprising: 2 use(s) of Ada2005 reserved words Source Filename: J:\SPARKworkspace\TimeT\time-interface.adb Listing Filename: J:\SPARKworkspace\TimeT\time-interface.lsb [View HTML] Unit name: Time.Interface Unit type: package body Unit has been analysed, any errors are listed below. No errors found 5 summarized warning(s), comprising: 1 hidden part(s)* 1 with clause(s) lacking a supporting inherit 3 use(s) of Ada2005 reserved words (*Note: the above warnings may affect the validity of the analysis.) Source Filename: J:\SPARKworkspace\TimeT\clock.ads Listing Filename: J:\SPARKworkspace\TimeT\clock.lss [View HTML] Unit name: Clock Unit type: package specification Unit has been analysed, any errors are listed below. No errors found 1 summarized warning(s), comprising: 1 use(s) of Ada2005 reserved words Source Filename: J:\SPARKworkspace\TimeT\clock.adb Listing Filename: J:\SPARKworkspace\TimeT\clock.lsb [View HTML] Unit name: Clock Unit type: package body Unit has been analysed, any errors are listed below. No errors found 2 summarized warning(s), comprising: 2 use(s) of Ada2005 reserved words --End of file--------------------------------------------------