32 lines
1.7 KiB
Plaintext
32 lines
1.7 KiB
Plaintext
/*********************************************************/
|
|
/*Proof Rule Declarations*/
|
|
/*Examiner GPL Edition*/
|
|
|
|
/*********************************************************/
|
|
|
|
|
|
/*procedure Spark_Dns_Main*/
|
|
|
|
|
|
rule_family spark_dns_ma_rules:
|
|
X requires [X:any] &
|
|
X <= Y requires [X:ire, Y:ire] &
|
|
X >= Y requires [X:ire, Y:ire].
|
|
|
|
spark_dns_ma_rules(1): spark_ada_command_line__failure may_be_replaced_by 1.
|
|
spark_dns_ma_rules(2): integer__size >= 0 may_be_deduced.
|
|
spark_dns_ma_rules(3): integer__first may_be_replaced_by -2147483648.
|
|
spark_dns_ma_rules(4): integer__last may_be_replaced_by 2147483647.
|
|
spark_dns_ma_rules(5): integer__base__first may_be_replaced_by -2147483648.
|
|
spark_dns_ma_rules(6): integer__base__last may_be_replaced_by 2147483647.
|
|
spark_dns_ma_rules(7): natural__size >= 0 may_be_deduced.
|
|
spark_dns_ma_rules(8): natural__first may_be_replaced_by 0.
|
|
spark_dns_ma_rules(9): natural__last may_be_replaced_by 2147483647.
|
|
spark_dns_ma_rules(10): natural__base__first may_be_replaced_by -2147483648.
|
|
spark_dns_ma_rules(11): natural__base__last may_be_replaced_by 2147483647.
|
|
spark_dns_ma_rules(12): spark_ada_command_line__exit_status__size >= 0 may_be_deduced.
|
|
spark_dns_ma_rules(13): spark_ada_command_line__exit_status__first may_be_replaced_by -2147483648.
|
|
spark_dns_ma_rules(14): spark_ada_command_line__exit_status__last may_be_replaced_by 2147483647.
|
|
spark_dns_ma_rules(15): spark_ada_command_line__exit_status__base__first may_be_replaced_by -2147483648.
|
|
spark_dns_ma_rules(16): spark_ada_command_line__exit_status__base__last may_be_replaced_by 2147483647.
|