102 lines
4.4 KiB
Plaintext
102 lines
4.4 KiB
Plaintext
*******************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
procedure Process_Dns_Request.Set_Unsigned_16
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 50:
|
|
|
|
procedure_set_unsigned_16_1.
|
|
H1: start_byte <= dns_types__packet_bytes_range__last - 1 .
|
|
H2: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
bytes, [i___1]) >= dns_types__byte__first) and (element(
|
|
bytes, [i___1]) <= dns_types__byte__last))) .
|
|
H3: start_byte >= dns_types__packet_bytes_range__first .
|
|
H4: start_byte <= dns_types__packet_bytes_range__last .
|
|
H5: value >= unsigned_types__unsigned16__first .
|
|
H6: value <= unsigned_types__unsigned16__last .
|
|
->
|
|
C1: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
C2: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
C3: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
C4: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
C5: 256 <> 0 .
|
|
C6: 2 ** 8 <> 0 .
|
|
C7: 2 ** 8 >= system__min_int .
|
|
C8: 2 ** 8 <= system__max_int .
|
|
C9: 8 >= 0 .
|
|
C10: start_byte >= dns_types__packet_bytes_range__first .
|
|
C11: start_byte <= dns_types__packet_bytes_range__last .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 51:
|
|
|
|
procedure_set_unsigned_16_2.
|
|
H1: start_byte <= dns_types__packet_bytes_range__last - 1 .
|
|
H2: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
bytes, [i___1]) >= dns_types__byte__first) and (element(
|
|
bytes, [i___1]) <= dns_types__byte__last))) .
|
|
H3: start_byte >= dns_types__packet_bytes_range__first .
|
|
H4: start_byte <= dns_types__packet_bytes_range__last .
|
|
H5: value >= unsigned_types__unsigned16__first .
|
|
H6: value <= unsigned_types__unsigned16__last .
|
|
H7: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
H8: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
H9: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
H10: value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod
|
|
unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
H11: 256 <> 0 .
|
|
H12: 2 ** 8 <> 0 .
|
|
H13: 2 ** 8 >= system__min_int .
|
|
H14: 2 ** 8 <= system__max_int .
|
|
H15: 8 >= 0 .
|
|
H16: start_byte >= dns_types__packet_bytes_range__first .
|
|
H17: start_byte <= dns_types__packet_bytes_range__last .
|
|
->
|
|
C1: value mod 256 mod unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
C2: value mod 256 mod unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
C3: value mod 256 mod unsigned_types__unsigned16__modulus >=
|
|
dns_types__byte__first .
|
|
C4: value mod 256 mod unsigned_types__unsigned16__modulus <=
|
|
dns_types__byte__last .
|
|
C5: 256 <> 0 .
|
|
C6: start_byte + 1 >= dns_types__packet_bytes_range__first .
|
|
C7: start_byte + 1 <= dns_types__packet_bytes_range__last .
|
|
C8: start_byte + 1 >= dns_types__packet_bytes_range__base__first .
|
|
C9: start_byte + 1 <= dns_types__packet_bytes_range__base__last .
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
procedure_set_unsigned_16_3.
|
|
*** true . /* trivially true VC removed by Examiner */
|
|
|
|
|