Skip to content

Commit 3bbafbe

Browse files
author
Thomas Kiley
authored
Merge pull request #330 from thk123/thk/order-properties
Update tests with ordered properties
2 parents 4f9729a + 166a788 commit 3bbafbe

File tree

21 files changed

+53
-53
lines changed

21 files changed

+53
-53
lines changed

‎lib/cbmc

Submodule cbmc updated 27 files

‎testsuite/gnat2goto/tests/address_clause/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,6 @@ N_Attribute_Definition_Clause "address" (Node_Id=2295) (source,analyzed)
1818
Entity = N_Defining_Identifier "var_addr_2" (Entity_Id=2282)
1919
Check_Address_Alignment = True
2020

21-
[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
2221
[address_clause.assertion.1] line 12 Ada Check assertion: SUCCESS
22+
[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
2323
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/arrays_access/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[arrays_access.assertion.1] line 5 Ada Check assertion: SUCCESS
55
[arrays_access.assertion.2] line 6 assertion Actual7(1) = 2: SUCCESS

‎testsuite/gnat2goto/tests/arrays_assign_nonoverlap/test.out

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
1-
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
2-
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
3-
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
4-
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
5-
[precondition_instance.14] file <internal> memcpy source region readable: SUCCESS
6-
[precondition_instance.13] file <internal> memcpy src/dst overlap: SUCCESS
7-
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
8-
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
9-
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
10-
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
11-
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
12-
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
13-
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
14-
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
151
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
162
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
173
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
184
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
195
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
6+
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
8+
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
9+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
10+
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
11+
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
12+
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
13+
[precondition_instance.13] file <internal> memcpy src/dst overlap: SUCCESS
14+
[precondition_instance.14] file <internal> memcpy source region readable: SUCCESS
15+
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
16+
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
17+
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
18+
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
2019
[precondition_instance.19] file <internal> memcpy src/dst overlap: SUCCESS
20+
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
2121
[precondition_instance.21] file <internal> memcpy destination region writeable: SUCCESS
2222
[arrays_assign_nonoverlap.assertion.1] line 8 Ada Check assertion: SUCCESS
2323
[arrays_assign_nonoverlap.assertion.2] line 8 assertion Full_Arr(1)=3: SUCCESS

‎testsuite/gnat2goto/tests/arrays_attributes_dynamic/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[array_consumer.assertion.1] line 7 assertion Arr'First = 1: SUCCESS
55
[array_consumer.assertion.2] line 8 assertion Arr'Last = 1: FAILURE

‎testsuite/gnat2goto/tests/arrays_attributes_static/test.out

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2-
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
3-
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
4-
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
5-
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
63
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4+
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
5+
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
6+
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
78
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
8-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
9-
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
109
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
1110
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
1211
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
@@ -16,6 +15,7 @@
1615
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
1716
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
1817
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
18+
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
1919
[arrays_attributes_static.assertion.1] line 12 Ada Check assertion: SUCCESS
2020
[arrays_attributes_static.assertion.2] line 16 assertion Array_Attribs = 41: SUCCESS
2121
[arrays_attributes_static.assertion.3] line 17 assertion An_Index = 12: SUCCESS

‎testsuite/gnat2goto/tests/arrays_concat/test.out

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
2-
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
3-
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
4-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
51
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
63
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
7-
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
84
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
95
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
106
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
117
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
128
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
9+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
10+
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
11+
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
12+
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
1313
[arrays_concat.assertion.1] line 7 Ada Check assertion: SUCCESS
1414
[arrays_concat.assertion.2] line 7 assertion Actual(2)=4: SUCCESS
1515
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/arrays_constraints/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[array_constraints.assertion.1] line 109 Ada Check assertion: SUCCESS
2-
[array_constraints.assertion.8] line 117 Ada Check assertion: SUCCESS
32
[array_constraints.assertion.2] line 117 assertion VUA1 (1) + VUA2 (2) + VUA3 (3) + VUA4 (4) + VUA5 (5) + VUA6 (6) + VUA7 (7) + VUA8 (8) = 36: SUCCESS
3+
[array_constraints.assertion.8] line 117 Ada Check assertion: SUCCESS
44
[array_constraints.assertion.3] line 131 assertion VCA1 (VCA1'Last) + VCA2 (VCA2'Last - 1) + VCA3 (VCA3'Last - 2) + VCA4 (Constrained_Array_4'Last - 3) = 10: SUCCESS
55
[array_constraints.assertion.4] line 143 assertion VEA1 (One) + VEA2 (Two) + VEA3 (Three) + VEA4 (Four) + VEA5 (Five) + VEA6 (Six) = 21: SUCCESS
66
[array_constraints.assertion.5] line 154 assertion VBA1 (False) + VBA2 (True) + VBA3 (False) + VBA4 (True) + VBA5 (False) + VBA6 (True) = 7: SUCCESS

‎testsuite/gnat2goto/tests/arrays_index/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[arrays_index.assertion.1] line 5 Ada Check assertion: SUCCESS
55
[arrays_index.assertion.2] line 9 assertion Actual(2) = 11: SUCCESS

‎testsuite/gnat2goto/tests/arrays_index_enum/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[test.assertion.1] line 7 Ada Check assertion: SUCCESS
55
[test.assertion.2] line 7 assertion Array_Value(Two) = 2: SUCCESS

‎testsuite/gnat2goto/tests/arrays_range/test.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
32
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
4-
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
54
[array_consumer.assertion.1] line 8 Ada Check assertion: SUCCESS
5+
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
66
[array_consumer.assertion.3] line 9 assertion An_Index = 2: SUCCESS
77
[array_consumer.assertion.4] line 11 assertion An_Index = 4: SUCCESS
88
[array_consumer.assertion.5] line 13 assertion An_Index = -1: SUCCESS

‎testsuite/gnat2goto/tests/arrays_write_element/test.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
2-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
31
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[arrays_write_element.assertion.1] line 6 Ada Check assertion: SUCCESS
55
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/attrib_address/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
32
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/enum_in_param/test.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
2-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
31
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[enum_in.assertion.1] line 23 Ada Check assertion: SUCCESS
55
[p_enum_in.assertion.1] line 19 assertion E in More_Than_Two: SUCCESS
66
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/expanded_name_subtype_indication/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
[test.assertion.2] line 8 assertion Val < 2.0: SUCCESS
22
[test.assertion.3] line 10 assertion Val > 0.0: SUCCESS
3-
[test.assertion.4] line 11 assertion Val * 20.0 < 10.0: FAILURE
43
[test.assertion.1] line 11 Ada Check assertion: SUCCESS
4+
[test.assertion.4] line 11 assertion Val * 20.0 < 10.0: FAILURE
55
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/if_integer/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[assertion.1] file divide.adb line 4 Ada Check assertion: SUCCESS
22
[divide.assertion.2] line 4 assertion B / 1 = B: SUCCESS
3-
[divide.assertion.3] line 6 assertion B / B = 1: SUCCESS
43
[divide.assertion.1] line 6 Ada Check assertion: SUCCESS
4+
[divide.assertion.3] line 6 assertion B / B = 1: SUCCESS
55
[divide.assertion.4] line 8 assertion B < 0: FAILURE
66
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/in_expression/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[in_expression.assertion.1] line 8 assertion Val < 1: FAILURE
55
[in_expression.assertion.2] line 10 assertion Val > 1: SUCCESS

‎testsuite/gnat2goto/tests/index_check/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
21
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[main.assertion.2] line 6 Ada Check assertion: FAILURE
55
[main.assertion.1] line 9 assertion AnArray(3)=6: SUCCESS

‎testsuite/gnat2goto/tests/package_type/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[package_type.assertion.2] line 8 assertion Small_Number * 2 = 8: SUCCESS
21
[package_type.assertion.1] line 8 Ada Check assertion: SUCCESS
2+
[package_type.assertion.2] line 8 assertion Small_Number * 2 = 8: SUCCESS
33
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/representation_clause_component_size/test.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
2-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
31
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[test.assertion.1] line 16 assertion My_Storage_Array(2)=2: SUCCESS
55
VERIFICATION SUCCESSFUL

‎testsuite/gnat2goto/tests/rhs_array_assign/test.out

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
2-
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
3-
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
4-
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
5-
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
6-
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
7-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
81
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
92
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4+
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
5+
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
6+
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
8+
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
9+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
1010
[rhs_array_assign.assertion.1] line 8 Ada Check assertion: SUCCESS
1111
[rhs_array_assign.assertion.2] line 9 assertion A (5) = 5 and A (1) = 0: SUCCESS
1212
VERIFICATION SUCCESSFUL

0 commit comments

Comments
 (0)