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

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


                 function Rr_Type.ConvertStringToDomainName




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

function_convertstringtodomainname_1.
H1:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
H2:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
        ->
C1:    s__index__subtype__1__last - s__index__subtype__1__first + 1 >= 
           integer__first .
C2:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           integer__last .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
 

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

function_convertstringtodomainname_2.
H1:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
H2:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    s__index__subtype__1__last - s__index__subtype__1__first + 1 >= 
           integer__first .
H4:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           integer__last .
H5:    1 >= integer__first .
H6:    1 <= integer__last .
        ->
C1:    (1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1) -> ((
           s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 >= integer__first) and (
           s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 <= integer__last)) .
C2:    (1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1) -> ((1 >= 
           integer__first) and (1 <= integer__last)) .
 

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

function_convertstringtodomainname_3.
H1:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
H2:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    s__index__subtype__1__last - s__index__subtype__1__first + 1 >= 
           integer__first .
H4:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           integer__last .
H5:    1 >= integer__first .
H6:    1 <= integer__last .
H7:    (1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1) -> ((
           s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 >= integer__first) and (
           s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 <= integer__last)) .
H8:    (1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1) -> ((1 >= 
           integer__first) and (1 <= integer__last)) .
H9:    1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C2:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
C5:    1 >= 1 .
C6:    1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 .
 

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

function_convertstringtodomainname_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
H3:    loop__1__i >= integer__first .
H4:    loop__1__i <= integer__last .
H5:    loop__1__i >= 1 .
H6:    loop__1__i <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 .
H7:    element(s, [loop__1__i]) >= character__first .
H8:    element(s, [loop__1__i]) <= character__last .
H9:    loop__1__i >= s__index__subtype__1__first .
H10:   loop__1__i <= s__index__subtype__1__last .
H11:   loop__1__i >= domainnamestringtypeindex__first .
H12:   loop__1__i <= domainnamestringtypeindex__last .
H13:   not (loop__1__i = s__index__subtype__1__last - 
           s__index__subtype__1__first + 1) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C2:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
C3:    loop__1__i + 1 >= integer__first .
C4:    loop__1__i + 1 <= integer__last .
C5:    loop__1__i + 1 >= 1 .
C6:    loop__1__i + 1 <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 .
 

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

function_convertstringtodomainname_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           s__index__subtype__1__first) and (i___1 <= 
           s__index__subtype__1__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    s__index__subtype__1__last - s__index__subtype__1__first + 1 <= 
           maxdomainnamelength .
H3:    loop__1__i >= integer__first .
H4:    loop__1__i <= integer__last .
H5:    loop__1__i >= 1 .
H6:    loop__1__i <= s__index__subtype__1__last - 
           s__index__subtype__1__first + 1 .
        ->
C1:    element(s, [loop__1__i]) >= character__first .
C2:    element(s, [loop__1__i]) <= character__last .
C3:    loop__1__i >= s__index__subtype__1__first .
C4:    loop__1__i <= s__index__subtype__1__last .
C5:    loop__1__i >= domainnamestringtypeindex__first .
C6:    loop__1__i <= domainnamestringtypeindex__last .
 

For path(s) from start to finish:

function_convertstringtodomainname_6.
*** true .          /* trivially true VC removed by Examiner */


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

function_convertstringtodomainname_7.
*** true .          /* trivially true VC removed by Examiner */


