Skip to content

Commit d57ab6e

Browse files
chrisr-diffbluechrisr-diffblue
authored
Merge pull request #323 from xbauch/feature/cbmc-bump
Bump CBMC to develop
2 parents 31d41fc + 5d359fd commit d57ab6e

File tree

29 files changed

+65
-65
lines changed

29 files changed

+65
-65
lines changed

‎lib/cbmc

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[symmetric_difference.assertion.1] line 3 Ada Check assertion: SUCCESS
21
[absolute.assertion.1] line 7 assertion Symmetric_Difference (X, Y) = Symmetric_Difference (Y, X): SUCCESS
32
[absolute.assertion.2] line 8 assertion Symmetric_Difference (X, Y) = 5: SUCCESS
43
[absolute.assertion.3] line 10 assertion Symmetric_Difference (Y, X) /= 5: FAILURE
4+
[symmetric_difference.assertion.1] line 3 Ada Check assertion: SUCCESS
55
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[symmetric_difference.assertion.1] line 3 Ada Check assertion: SUCCESS
21
[absolute_float.assertion.1] line 7 assertion Symmetric_Difference (X, Y) = Symmetric_Difference (Y, X): SUCCESS
32
[absolute_float.assertion.2] line 8 assertion Symmetric_Difference (X, Y) = 5.0: SUCCESS
43
[absolute_float.assertion.3] line 10 assertion Symmetric_Difference (Y, X) /= 5.0: FAILURE
4+
[symmetric_difference.assertion.1] line 3 Ada Check assertion: SUCCESS
55
VERIFICATION FAILED

‎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.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,24 @@
1-
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2-
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
3-
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
4-
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
5-
[precondition_instance.13] file <internal> memcpy src/dst overlap: SUCCESS
6-
[precondition_instance.14] file <internal> memcpy source region readable: SUCCESS
7-
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
8-
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
1+
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
92
[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
1013
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
11-
[precondition_instance.19] file <internal> memcpy src/dst overlap: SUCCESS
14+
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
15+
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
1216
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
13-
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
14-
[precondition_instance.21] file <internal> memcpy destination region writeable: SUCCESS
1517
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
1618
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
1719
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
18-
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
19-
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
20-
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
21-
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
20+
[precondition_instance.19] file <internal> memcpy src/dst overlap: SUCCESS
21+
[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
2424
[arrays_assign_nonoverlap.assertion.3] line 9 assertion Full_Arr(2)=4: 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.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,13 @@
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
6+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
7+
[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
10+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
211
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
312
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
413
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
@@ -7,15 +16,6 @@
716
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
817
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
918
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
10-
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
11-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
12-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
13-
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
14-
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
15-
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
16-
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
17-
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
18-
[precondition_instance.9] 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: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2-
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
3-
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
41
[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
54
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
5+
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
66
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
78
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
89
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
910
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
1011
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
1112
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
12-
[precondition_instance.9] 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_index/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
12
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
23
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3-
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
55
[array_consumer.assertion.1] line 8 Ada Check assertion: SUCCESS
66
[array_consumer.assertion.3] line 9 assertion An_Index = 2: 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.1] file <internal> memcpy src/dst overlap: SUCCESS
2-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
31
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
44
[arrays_write_element.assertion.1] line 6 Ada Check assertion: SUCCESS
55
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[check.assertion.1] line 15 assertion X = 5: FAILURE
22
[check2.assertion.1] line 20 assertion False or (X < 10 and X > 0): SUCCESS
3-
[plus.assertion.1] line 28 Ada Check assertion: SUCCESS
43
[check3.assertion.1] line 32 assertion Plus (X, Plus (X, 1)) <= 15 and Plus (X => X, Y => -5) >= -5: FAILURE
54
[check4.assertion.1] line 43 assertion X < 10: FAILURE
5+
[plus.assertion.1] line 28 Ada Check assertion: SUCCESS
66
VERIFICATION FAILED

‎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
12
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
23
[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/divide_by_zero/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1+
[assertion.1] file divide_by_zero.adb line 6 Ada Check assertion: FAILURE
12
[divide_by_zero.assertion.1] line 6 Ada Check assertion: FAILURE
2-
[assertion.1] line 6 Ada Check assertion: FAILURE
33
VERIFICATION FAILED

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

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

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[check_assoc_int_minusR.assertion.1] line 10 assertion (A + (B + C)) = ((A + B) + C): FAILURE
21
[check_assoc_intR.assertion.1] line 10 Ada Check assertion: FAILURE
32
[check_assoc_intR.assertion.2] line 10 assertion (A + (B + C)) = ((A + B) + C): SUCCESS
3+
[check_assoc_int_minusR.assertion.1] line 10 assertion (A + (B + C)) = ((A + B) + C): FAILURE
44
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1+
[assertion.1] file divide.adb line 4 Ada Check assertion: SUCCESS
12
[divide.assertion.2] line 4 assertion B / 1 = B: SUCCESS
2-
[assertion.1] line 4 Ada Check assertion: SUCCESS
33
[divide.assertion.3] line 6 assertion B / B = 1: SUCCESS
44
[divide.assertion.1] line 6 Ada Check assertion: SUCCESS
55
[divide.assertion.4] line 8 assertion B < 0: FAILURE

‎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.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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.1] file <internal> memcpy src/dst overlap: SUCCESS
21
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
2+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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/mixed_parameters/test.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
[subtract.assertion.1] line 5 Ada Check assertion: SUCCESS
21
[mixed_parameters.assertion.1] line 10 assertion C = 1: SUCCESS
32
[mixed_parameters.assertion.2] line 12 assertion C = 0: SUCCESS
43
[mixed_parameters.assertion.3] line 14 assertion C = 5: SUCCESS
54
[mixed_parameters.assertion.4] line 16 assertion C = 2: SUCCESS
65
[mixed_parameters.assertion.5] line 18 assertion C /= 0: FAILURE
6+
[subtract.assertion.1] line 5 Ada Check assertion: SUCCESS
77
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1+
[assertion.1] file op_or_else.adb line 16 Ada Check assertion: FAILURE
12
[div_by_zero.assertion.1] line 16 Ada Check assertion: FAILURE
2-
[assertion.1] line 16 Ada Check assertion: FAILURE
33
[op_or_else.assertion.1] line 34 assertion A or else B: SUCCESS
44
[op_or_else.assertion.2] line 35 assertion B or else A: SUCCESS
55
[op_or_else.assertion.3] line 36 assertion A or else A: SUCCESS

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[timer_interrupt.assertion.1] line 12 Ada Check assertion: SUCCESS
21
[pragma_machine_attribute.assertion.1] line 21 assertion Timeout and Interval = Seconds_Count: SUCCESS
2+
[timer_interrupt.assertion.1] line 12 Ada Check assertion: SUCCESS
33
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[increment_by.assertion.1] line 5 Ada Check assertion: SUCCESS
21
[assert_modify.assertion.1] line 17 assertion Global_Number = 5: FAILURE
2+
[increment_by.assertion.1] line 5 Ada Check assertion: SUCCESS
33
VERIFICATION FAILED

‎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.1] file <internal> memcpy src/dst overlap: SUCCESS
2-
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
31
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.1] file <internal> memcpy src/dst overlap: 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.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
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
81
[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
96
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
8+
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
9+
[precondition_instance.2] file <internal> memcpy source region readable: 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

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
[sum_plus_three.assertion.1] line 11 Ada Check assertion: SUCCESS
2-
[sum_plus_three.assertion.2] line 12 assertion Local1=3: SUCCESS
31
[statement_block.assertion.1] line 30 assertion Var2=2: SUCCESS
42
[statement_block.assertion.2] line 35 assertion Var2=4: SUCCESS
53
[statement_block.assertion.3] line 45 assertion Var2=10: SUCCESS
4+
[sum_plus_three.assertion.1] line 11 Ada Check assertion: SUCCESS
5+
[sum_plus_three.assertion.2] line 12 assertion Local1=3: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
[assertion.1] file modular_type.adb line 28 Ada Check assertion: SUCCESS
12
[assert_val.assertion.1] line 6 assertion X = 5: SUCCESS
23
[assert_val.assertion.2] line 8 assertion X + 3 = 8: SUCCESS
34
[assert_val.assertion.3] line 9 assertion X + 6 = 1: SUCCESS
@@ -16,6 +17,5 @@
1617
[assert_val.assertion.16] line 23 assertion Y * 8 = 2: SUCCESS
1718
[assert_val.assertion.17] line 24 assertion Y * 9 = 6: SUCCESS
1819
[assert_val.assertion.18] line 26 assertion X - 6 = 9: SUCCESS
19-
[assertion.1] line 28 Ada Check assertion: SUCCESS
2020
[assert_val.assertion.19] line 28 assertion X / 2 = 2: SUCCESS
2121
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[negate.assertion.1] line 9 Ada Check assertion: SUCCESS
21
[minus.assertion.1] line 15 assertion Large_Negative = 2: FAILURE
2+
[negate.assertion.1] line 9 Ada Check assertion: SUCCESS
33
VERIFICATION FAILED

0 commit comments

Comments
 (0)