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

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


                      function Rr_Type.WireNameLength




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

function_wirenamelength_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
        ->
C1:    wirestringtypeindex__first >= wirestringtypeindex__first .
C2:    wirestringtypeindex__first <= wirestringtypeindex__last .
 

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

function_wirenamelength_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H2:    wirestringtypeindex__first >= wirestringtypeindex__first .
H3:    wirestringtypeindex__first <= wirestringtypeindex__last .
H4:    wirestringtypeindex__first >= wirestringtypeindex__first .
H5:    wirestringtypeindex__first <= wirestringtypeindex__last .
        ->
C1:    0 >= character__first .
C2:    0 <= character__last .
C3:    wirestringtypeindex__first >= wirestringtypeindex__first .
C4:    wirestringtypeindex__first <= wirestringtypeindex__last .
C5:    maxdomainnamelength + 1 >= integer__base__first .
C6:    maxdomainnamelength + 1 <= integer__base__last .
 

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

function_wirenamelength_3.
H1:    index < maxdomainnamelength + 1 .
H2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= index)) -> (element(
           name, [q_]) <> 0)) .
H3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H4:    index >= wirestringtypeindex__first .
H5:    index <= wirestringtypeindex__last .
H6:    index + 1 >= wirestringtypeindex__first .
H7:    index + 1 <= wirestringtypeindex__last .
H8:    index + 1 >= wirestringtypeindex__first .
H9:    index + 1 <= wirestringtypeindex__last .
        ->
C1:    0 >= character__first .
C2:    0 <= character__last .
C3:    index + 1 >= wirestringtypeindex__first .
C4:    index + 1 <= wirestringtypeindex__last .
C5:    maxdomainnamelength + 1 >= integer__base__first .
C6:    maxdomainnamelength + 1 <= integer__base__last .
 

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

function_wirenamelength_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H2:    wirestringtypeindex__first >= wirestringtypeindex__first .
H3:    wirestringtypeindex__first <= wirestringtypeindex__last .
H4:    wirestringtypeindex__first >= wirestringtypeindex__first .
H5:    wirestringtypeindex__first <= wirestringtypeindex__last .
H6:    0 >= character__first .
H7:    0 <= character__last .
H8:    wirestringtypeindex__first >= wirestringtypeindex__first .
H9:    wirestringtypeindex__first <= wirestringtypeindex__last .
H10:   maxdomainnamelength + 1 >= integer__base__first .
H11:   maxdomainnamelength + 1 <= integer__base__last .
H12:   wirestringtypeindex__first < maxdomainnamelength + 1 .
H13:   element(name, [wirestringtypeindex__first]) <> 0 .
        ->
C1:    wirestringtypeindex__first < maxdomainnamelength + 1 .
C2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= 
           wirestringtypeindex__first)) -> (element(name, [
           q_]) <> 0)) .
C3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
 

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

function_wirenamelength_5.
H1:    index < maxdomainnamelength + 1 .
H2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= index)) -> (element(
           name, [q_]) <> 0)) .
H3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H4:    index >= wirestringtypeindex__first .
H5:    index <= wirestringtypeindex__last .
H6:    index + 1 >= wirestringtypeindex__first .
H7:    index + 1 <= wirestringtypeindex__last .
H8:    index + 1 >= wirestringtypeindex__first .
H9:    index + 1 <= wirestringtypeindex__last .
H10:   0 >= character__first .
H11:   0 <= character__last .
H12:   index + 1 >= wirestringtypeindex__first .
H13:   index + 1 <= wirestringtypeindex__last .
H14:   maxdomainnamelength + 1 >= integer__base__first .
H15:   maxdomainnamelength + 1 <= integer__base__last .
H16:   index + 1 < maxdomainnamelength + 1 .
H17:   element(name, [index + 1]) <> 0 .
        ->
C1:    index + 1 < maxdomainnamelength + 1 .
C2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= index + 1)) -> (element(
           name, [q_]) <> 0)) .
C3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
 

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

function_wirenamelength_6.
H1:    index < maxdomainnamelength + 1 .
H2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= index)) -> (element(
           name, [q_]) <> 0)) .
H3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H4:    index >= wirestringtypeindex__first .
H5:    index <= wirestringtypeindex__last .
        ->
C1:    index + 1 >= wirestringtypeindex__first .
C2:    index + 1 <= wirestringtypeindex__last .
 

For path(s) from start to finish:

function_wirenamelength_7.
H1:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H2:    wirestringtypeindex__first >= wirestringtypeindex__first .
H3:    wirestringtypeindex__first <= wirestringtypeindex__last .
H4:    wirestringtypeindex__first >= wirestringtypeindex__first .
H5:    wirestringtypeindex__first <= wirestringtypeindex__last .
H6:    0 >= character__first .
H7:    0 <= character__last .
H8:    wirestringtypeindex__first >= wirestringtypeindex__first .
H9:    wirestringtypeindex__first <= wirestringtypeindex__last .
H10:   maxdomainnamelength + 1 >= integer__base__first .
H11:   maxdomainnamelength + 1 <= integer__base__last .
H12:   not ((wirestringtypeindex__first < 
           maxdomainnamelength + 1) and (element(name, [
           wirestringtypeindex__first]) <> 0)) .
H13:   wirestringtypeindex__first >= wirestringtypeindex__first .
H14:   wirestringtypeindex__first <= wirestringtypeindex__last .
        ->
C1:    (wirestringtypeindex__first = maxdomainnamelength + 1) or ((element(
           name, [wirestringtypeindex__first]) = 0) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           wirestringtypeindex__first - 1)) -> (element(
           name, [q_]) <> 0)))) .
C2:    wirestringtypeindex__first >= wirestringtypeindex__first .
C3:    wirestringtypeindex__first <= wirestringtypeindex__last .
 

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

function_wirenamelength_8.
H1:    index < maxdomainnamelength + 1 .
H2:    for_all(q_: integer, ((q_ >= 1) and (q_ <= index)) -> (element(
           name, [q_]) <> 0)) .
H3:    for_all(i___1: integer, ((i___1 >= 
           wirestringtypeindex__first) and (i___1 <= 
           wirestringtypeindex__last)) -> ((element(name, [
           i___1]) >= character__first) and (element(name, [
           i___1]) <= character__last))) .
H4:    index >= wirestringtypeindex__first .
H5:    index <= wirestringtypeindex__last .
H6:    index + 1 >= wirestringtypeindex__first .
H7:    index + 1 <= wirestringtypeindex__last .
H8:    index + 1 >= wirestringtypeindex__first .
H9:    index + 1 <= wirestringtypeindex__last .
H10:   0 >= character__first .
H11:   0 <= character__last .
H12:   index + 1 >= wirestringtypeindex__first .
H13:   index + 1 <= wirestringtypeindex__last .
H14:   maxdomainnamelength + 1 >= integer__base__first .
H15:   maxdomainnamelength + 1 <= integer__base__last .
H16:   not ((index + 1 < maxdomainnamelength + 1) and (element(
           name, [index + 1]) <> 0)) .
H17:   index + 1 >= wirestringtypeindex__first .
H18:   index + 1 <= wirestringtypeindex__last .
        ->
C1:    (index + 1 = maxdomainnamelength + 1) or ((element(
           name, [index + 1]) = 0) and (for_all(q_: integer, ((
           q_ >= 1) and (q_ <= index + 1 - 1)) -> (element(
           name, [q_]) <> 0)))) .
C2:    index + 1 >= wirestringtypeindex__first .
C3:    index + 1 <= wirestringtypeindex__last .
 

