*****************************************************************************
                       Semantic Analysis of SPARK Text
 SPARK Examiner Pro Edition, Version 8.1.0, Build Date 20090416, Build 13003
      Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K.
*****************************************************************************


CREATED 07-MAY-2009, 11:51:57  SIMPLIFIED 07-MAY-2009, 11:52:46

SPARK Simplifier Pro Edition, Version 8.1.0, Build Date 20090424, Build 
Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K.

procedure ConfigData.ValidateFile.ReadDuration




For path(s) from start to run-time check associated with statement of line 220:

procedure_readduration_1.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 221:

procedure_readduration_2.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 221:

procedure_readduration_3.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 233:

procedure_readduration_4.
H1:    rawduration__1 >= - 2147483648 .
H2:    rawduration__1 <= 2147483647 .
H3:    integer__size >= 0 .
H4:    natural__size >= 0 .
H5:    positive__size >= 0 .
H6:    clock__durationt__size >= 0 .
H7:    clock__durationt__base__first <= clock__durationt__base__last .
H8:    durationt__size >= 0 .
H9:    durationt__base__first <= durationt__base__last .
H10:   clock__durationt__base__first <= 0 .
H11:   clock__durationt__base__last >= 864000 .
H12:   durationt__base__first <= 0 .
H13:   durationt__base__last >= 2000 .
       ->
C1:    success__1 -> rawduration__1 * 10 >= - 2147483648 and rawduration__1 * 
          10 <= 2147483647 .


For path(s) from start to run-time check associated with statement of line 237:

procedure_readduration_5.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 243:

procedure_readduration_6.
*** true .          /* all conclusions proved */


procedure_readduration_7.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

procedure_readduration_8.
*** true .          /* all conclusions proved */


procedure_readduration_9.
*** true .          /* all conclusions proved */


procedure_readduration_10.
*** true .          /* all conclusions proved */


procedure_readduration_11.
*** true .          /* all conclusions proved */