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