*****************************************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

*****************************************************************************



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

function Rr_Type.DomainNameLength




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

function_domainnamelength_1.
*** true .          /* all conclusions proved */


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

function_domainnamelength_2.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 33 to run-time check associated with 
          statement of line 32:

function_domainnamelength_3.
*** true .          /* all conclusions proved */


For path(s) from start to assertion of line 33:

function_domainnamelength_4.
H1:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
          name, [i___1]) and element(name, [i___1]) <= 255) .
H2:    element(name, [1]) <> 32 .
H3:    element(name, [2]) <> 32 .
H4:    integer__size >= 0 .
H5:    character__size >= 0 .
H6:    positive__size >= 0 .
H7:    domainnamestringtypeindex__size >= 0 .
       ->
C1:    for_all(q_ : integer, 1 <= q_ and q_ <= 2 -> element(name, [q_]) <> 32) .


For path(s) from assertion of line 33 to assertion of line 33:

function_domainnamelength_5.
H1:    for_all(q_ : integer, 1 <= q_ and q_ <= index + 1 -> element(name, [q_]) 
          <> 32) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
          name, [i___1]) and element(name, [i___1]) <= 255) .
H3:    index >= 1 .
H4:    index < 127 .
H5:    element(name, [1]) <> 32 .
H6:    element(name, [index + 2]) <> 32 .
H7:    index >= - 1 .
H8:    index <= 126 .
H9:    index >= - 2147483650 .
H10:   index <= 2147483645 .
H11:   integer__size >= 0 .
H12:   character__size >= 0 .
H13:   positive__size >= 0 .
H14:   domainnamestringtypeindex__size >= 0 .
       ->
C1:    for_all(q_ : integer, 1 <= q_ and q_ <= index + 2 -> element(name, [q_]) 
          <> 32) .


For path(s) from assertion of line 33 to run-time check associated with 
          statement of line 35:

function_domainnamelength_6.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

function_domainnamelength_7.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 33 to finish:

function_domainnamelength_8.
H1:    index < 128 .
H2:    for_all(q_ : integer, 1 <= q_ and q_ <= index + 1 -> element(name, [q_]) 
          <> 32) .
H3:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
          name, [i___1]) and element(name, [i___1]) <= 255) .
H4:    index >= 1 .
H5:    index < 127 and element(name, [1]) <> 32 -> index >= - 1 and index <= 
          126 .
H6:    index < 127 and element(name, [1]) <> 32 -> index >= - 2147483650 and 
          index <= 2147483645 .
H7:    127 <= index or element(name, [index + 2]) = 32 .
H8:    integer__size >= 0 .
H9:    character__size >= 0 .
H10:   positive__size >= 0 .
H11:   domainnamestringtypeindex__size >= 0 .
       ->
C1:    index = 127 or element(name, [index + 2]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= index + 1 -> element(name, [q_]) <> 32) .


