Skip to content

Commit 1038feb

Browse files
petr-bauchpetr-bauch
committed
Include function info in assertions
It was missing in the index/range/etc. checks.
1 parent 97d3791 commit 1038feb

File tree

72 files changed

+164
-155
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

72 files changed

+164
-155
lines changed

‎gnat2goto/driver/goto_utils.adb

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1018,4 +1018,26 @@ package body GOTO_Utils is
10181018
Range_Check => Range_Check);
10191019
end Make_Let_Binding_Expr;
10201020

1021+
function Get_Context_Name (Intermediate_Node : Node_Id)
1022+
return String is
1023+
begin
1024+
if not (Present (Intermediate_Node)) then
1025+
return "";
1026+
end if;
1027+
case Nkind (Intermediate_Node) is
1028+
when N_Subprogram_Body =>
1029+
return Get_Name_String
1030+
(Chars
1031+
(Defining_Unit_Name
1032+
(Specification
1033+
(Intermediate_Node))));
1034+
when N_Package_Body =>
1035+
return Get_Name_String
1036+
(Chars
1037+
(Defining_Unit_Name
1038+
(Intermediate_Node)));
1039+
when others =>
1040+
return Get_Context_Name (Parent (Intermediate_Node));
1041+
end case;
1042+
end Get_Context_Name;
10211043
end GOTO_Utils;

‎gnat2goto/driver/goto_utils.ads

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -238,4 +238,9 @@ package GOTO_Utils is
238238
I_Type : Irep := Ireps.Empty;
239239
Range_Check : Boolean := False)
240240
return Irep;
241+
242+
-- return name of containing function or package
243+
-- (whichever comes earlier)
244+
function Get_Context_Name (Intermediate_Node : Node_Id)
245+
return String;
241246
end GOTO_Utils;

‎gnat2goto/driver/range_check.adb

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -428,6 +428,7 @@ package body Range_Check is
428428
Source_Location => Get_Source_Location (N),
429429
I_Type => Expected_Return_Type);
430430
begin
431+
Set_Function (Source_Loc, Get_Context_Name (N));
431432
pragma Assert (Underlying_Lower_Type = Underlying_Upper_Type);
432433

433434
Append_Argument (Call_Args,

‎gnat2goto/driver/tree_walk.adb

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2507,25 +2507,6 @@ package body Tree_Walk is
25072507
function Make_Assert_Comment return Irep;
25082508
function Make_Assert_Comment return Irep
25092509
is
2510-
-- return name of containing function or package
2511-
-- (whichever comes earlier)
2512-
function Get_Context_Name (Intermediate_Node : Node_Id)
2513-
return String;
2514-
function Get_Context_Name (Intermediate_Node : Node_Id)
2515-
return String is
2516-
begin
2517-
case Nkind (Intermediate_Node) is
2518-
when N_Subprogram_Body | N_Package_Body =>
2519-
return Get_Name_String
2520-
(Chars
2521-
(Defining_Unit_Name
2522-
(Specification
2523-
(Intermediate_Node))));
2524-
when others =>
2525-
return Get_Context_Name (Parent (Intermediate_Node));
2526-
end case;
2527-
end Get_Context_Name;
2528-
25292510
Source_Loc : constant Irep := Get_Source_Location (N);
25302511
Context_Name : constant String := Get_Context_Name (N);
25312512
Comment_Prefix : constant String := "assertion ";

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

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

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[assertion.1] file absolute_float.adb line 3 Ada Check assertion: SUCCESS
1+
[symmetric_difference.assertion.1] line 3 Ada Check assertion: SUCCESS
22
[absolute_float.assertion.1] line 7 assertion Symmetric_Difference (X, Y) = Symmetric_Difference (Y, X): SUCCESS
33
[absolute_float.assertion.2] line 8 assertion Symmetric_Difference (X, Y) = 5.0: SUCCESS
44
[absolute_float.assertion.3] line 10 assertion Symmetric_Difference (Y, X) /= 5.0: FAILURE

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

Lines changed: 2 additions & 2 deletions
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.1] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
22-
[assertion.1] line 12 Ada Check assertion: SUCCESS
21+
[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
22+
[address_clause.assertion.1] line 12 Ada Check assertion: SUCCESS
2323
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4-
[assertion.1] file arrays_access.adb line 5 Ada Check assertion: SUCCESS
5-
[arrays_access.assertion.1] line 6 assertion Actual7(1) = 2: SUCCESS
4+
[arrays_access.assertion.1] line 5 Ada Check assertion: SUCCESS
5+
[arrays_access.assertion.2] line 6 assertion Actual7(1) = 2: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@
1919
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
2020
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
2121
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
22-
[assertion.1] file arrays_assign_nonoverlap.adb line 8 Ada Check assertion: SUCCESS
23-
[arrays_assign_nonoverlap.assertion.1] line 8 assertion Full_Arr(1)=3: SUCCESS
24-
[arrays_assign_nonoverlap.assertion.2] line 9 assertion Full_Arr(2)=4: SUCCESS
25-
[arrays_assign_nonoverlap.assertion.3] line 10 assertion Full_Arr(3)=1: SUCCESS
26-
[arrays_assign_nonoverlap.assertion.4] line 11 assertion Full_Arr(4)=2: SUCCESS
22+
[arrays_assign_nonoverlap.assertion.1] line 8 Ada Check assertion: SUCCESS
23+
[arrays_assign_nonoverlap.assertion.2] line 8 assertion Full_Arr(1)=3: SUCCESS
24+
[arrays_assign_nonoverlap.assertion.3] line 9 assertion Full_Arr(2)=4: SUCCESS
25+
[arrays_assign_nonoverlap.assertion.4] line 10 assertion Full_Arr(3)=1: SUCCESS
26+
[arrays_assign_nonoverlap.assertion.5] line 11 assertion Full_Arr(4)=2: SUCCESS
2727
VERIFICATION SUCCESSFUL

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
1717
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
1818
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
19-
[assertion.1] file arrays_attributes_static.adb line 12 Ada Check assertion: SUCCESS
20-
[arrays_attributes_static.assertion.1] line 16 assertion Array_Attribs = 41: SUCCESS
21-
[arrays_attributes_static.assertion.2] line 17 assertion An_Index = 12: SUCCESS
19+
[arrays_attributes_static.assertion.1] line 12 Ada Check assertion: SUCCESS
20+
[arrays_attributes_static.assertion.2] line 16 assertion Array_Attribs = 41: SUCCESS
21+
[arrays_attributes_static.assertion.3] line 17 assertion An_Index = 12: SUCCESS
2222
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,6 @@
1010
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
1111
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
1212
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
13-
[assertion.1] file arrays_concat.adb line 7 Ada Check assertion: SUCCESS
14-
[arrays_concat.assertion.1] line 7 assertion Actual(2)=4: SUCCESS
13+
[arrays_concat.assertion.1] line 7 Ada Check assertion: SUCCESS
14+
[arrays_concat.assertion.2] line 7 assertion Actual(2)=4: SUCCESS
1515
VERIFICATION SUCCESSFUL

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
[assertion.1] file array_constraints.adb line 109 Ada Check assertion: SUCCESS
2-
[assertion.2] file array_constraints.adb line 117 Ada Check assertion: SUCCESS
3-
[array_constraints.assertion.1] line 117 assertion VUA1 (1) + VUA2 (2) + VUA3 (3) + VUA4 (4) + VUA5 (5) + VUA6 (6) + VUA7 (7) + VUA8 (8) = 36: SUCCESS
4-
[array_constraints.assertion.2] line 131 assertion VCA1 (VCA1'Last) + VCA2 (VCA2'Last - 1) + VCA3 (VCA3'Last - 2) + VCA4 (Constrained_Array_4'Last - 3) = 10: SUCCESS
5-
[array_constraints.assertion.3] line 143 assertion VEA1 (One) + VEA2 (Two) + VEA3 (Three) + VEA4 (Four) + VEA5 (Five) + VEA6 (Six) = 21: SUCCESS
6-
[array_constraints.assertion.4] line 154 assertion VBA1 (False) + VBA2 (True) + VBA3 (False) + VBA4 (True) + VBA5 (False) + VBA6 (True) = 7: SUCCESS
7-
[array_constraints.assertion.5] line 166 assertion VAC1 ('A') + VAC3 ('b') + VAC4 ('c') + VAC5 ('0') + VAC6 ('x') + VAC8 ('e') + VAC9 ('f') = 36: SUCCESS
8-
[array_constraints.assertion.6] line 180 assertion VAM1 (1) + VAM2 (2) + VAM3 (3) + VAM4 (4) + VAM5 (5) + VAM6 (6) + VAM7 (7) + VAM8 (8) + VAM9 (9) = 45: SUCCESS
1+
[array_constraints.assertion.1] line 109 Ada Check assertion: SUCCESS
2+
[array_constraints.assertion.8] line 117 Ada Check assertion: SUCCESS
3+
[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
4+
[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
5+
[array_constraints.assertion.4] line 143 assertion VEA1 (One) + VEA2 (Two) + VEA3 (Three) + VEA4 (Four) + VEA5 (Five) + VEA6 (Six) = 21: SUCCESS
6+
[array_constraints.assertion.5] line 154 assertion VBA1 (False) + VBA2 (True) + VBA3 (False) + VBA4 (True) + VBA5 (False) + VBA6 (True) = 7: SUCCESS
7+
[array_constraints.assertion.6] line 166 assertion VAC1 ('A') + VAC3 ('b') + VAC4 ('c') + VAC5 ('0') + VAC6 ('x') + VAC8 ('e') + VAC9 ('f') = 36: SUCCESS
8+
[array_constraints.assertion.7] line 180 assertion VAM1 (1) + VAM2 (2) + VAM3 (3) + VAM4 (4) + VAM5 (5) + VAM6 (6) + VAM7 (7) + VAM8 (8) + VAM9 (9) = 45: SUCCESS
99
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4-
[assertion.1] file arrays_index.adb line 5 Ada Check assertion: SUCCESS
5-
[arrays_index.assertion.1] line 9 assertion Actual(2) = 11: SUCCESS
4+
[arrays_index.assertion.1] line 5 Ada Check assertion: SUCCESS
5+
[arrays_index.assertion.2] line 9 assertion Actual(2) = 11: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4-
[assertion.1] file test.adb line 7 Ada Check assertion: SUCCESS
5-
[test.assertion.1] line 7 assertion Array_Value(Two) = 2: SUCCESS
4+
[test.assertion.1] line 7 Ada Check assertion: SUCCESS
5+
[test.assertion.2] line 7 assertion Array_Value(Two) = 2: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4-
[assertion.2] file arrays_range.adb line 8 Ada Check assertion: FAILURE
5-
[assertion.1] file arrays_range.adb line 8 Ada Check assertion: SUCCESS
6-
[array_consumer.assertion.1] line 9 assertion An_Index = 2: SUCCESS
7-
[array_consumer.assertion.2] line 11 assertion An_Index = 4: SUCCESS
8-
[array_consumer.assertion.3] line 13 assertion An_Index = -1: SUCCESS
4+
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
5+
[array_consumer.assertion.1] line 8 Ada Check assertion: SUCCESS
6+
[array_consumer.assertion.3] line 9 assertion An_Index = 2: SUCCESS
7+
[array_consumer.assertion.4] line 11 assertion An_Index = 4: SUCCESS
8+
[array_consumer.assertion.5] line 13 assertion An_Index = -1: SUCCESS
99
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4-
[assertion.1] file arrays_write_element.adb line 6 Ada Check assertion: SUCCESS
4+
[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-
[assertion.1] line 28 Ada Check assertion: SUCCESS
3+
[plus.assertion.1] line 28 Ada Check assertion: SUCCESS
44
[check3.assertion.1] line 32 assertion Plus (X, Plus (X, 1)) <= 15 and Plus (X => X, Y => -5) >= -5: FAILURE
55
[check4.assertion.1] line 43 assertion X < 10: FAILURE
66
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
[assign.assertion.1] line 6 assertion a = 1: SUCCESS
22
[assign.assertion.2] line 7 assertion b = 2: SUCCESS
3-
[assertion.1] line 8 Ada Check assertion: SUCCESS
3+
[assign.assertion.3] line 8 Ada Check assertion: SUCCESS
44
VERIFICATION SUCCESSFUL

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[assertion.2] file test.adb line 6 Ada Exception: FAILURE
2-
[assertion.1] file test.adb line 16 Ada Check assertion: SUCCESS
3-
[test.assertion.1] line 25 assertion Error_Count = 1: SUCCESS
1+
[assertion.1] file test.adb line 6 Ada Exception: FAILURE
2+
[test.assertion.1] line 16 Ada Check assertion: SUCCESS
3+
[test.assertion.2] line 25 assertion Error_Count = 1: SUCCESS
44
VERIFICATION FAILED

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
Error from cbmc test:
2-
function '__CPROVER_Ada_Overflow_Check' in module '' is shadowed by a definition in module ''
32
function '__range_check_const_decs.5' in module '' is shadowed by a definition in module ''
3+
function '__CPROVER_Ada_Overflow_Check' in module '' is shadowed by a definition in module ''
44

55
[assertion.1] file const_decs.ads line 8 Ada Check assertion: FAILURE
66
[test.assertion.1] line 8 assertion My_P = 50: FAILURE

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
[assertion.1] file declaration_rename.adb line 25 Ada Check assertion: SUCCESS
2-
[declaration_rename.assertion.1] line 28 assertion B=3: SUCCESS
3-
[declaration_rename.assertion.2] line 29 assertion Simply_Named_Int=11: SUCCESS
4-
[declaration_rename.assertion.3] line 30 assertion My_Plus(A,B)=5: SUCCESS
5-
[declaration_rename.assertion.4] line 31 assertion C=4: SUCCESS
1+
[declaration_rename.assertion.1] line 25 Ada Check assertion: SUCCESS
2+
[declaration_rename.assertion.2] line 28 assertion B=3: SUCCESS
3+
[declaration_rename.assertion.3] line 29 assertion Simply_Named_Int=11: SUCCESS
4+
[declaration_rename.assertion.4] line 30 assertion My_Plus(A,B)=5: SUCCESS
5+
[declaration_rename.assertion.5] line 31 assertion C=4: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[assertion.1] file deferred_const.adb line 4 Ada Check assertion: SUCCESS
1+
[inc.assertion.1] line 4 Ada Check assertion: SUCCESS
22
[test.assertion.1] line 6 assertion My_P = 4: SUCCESS
33
VERIFICATION SUCCESSFUL

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[assertion.1] file discriminated_record.adb line 16 Ada Check assertion: SUCCESS
2-
[discriminated_record.assertion.1] line 19 assertion Inst1.A (5) = 1: SUCCESS
3-
[discriminated_record.assertion.2] line 21 assertion Inst1.A (5) = 1: SUCCESS
1+
[discriminated_record.assertion.1] line 16 Ada Check assertion: SUCCESS
2+
[discriminated_record.assertion.2] line 19 assertion Inst1.A (5) = 1: SUCCESS
3+
[discriminated_record.assertion.3] line 21 assertion Inst1.A (5) = 1: SUCCESS
44
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
[assertion.1] file divide.adb line 6 Ada Check assertion: SUCCESS
2-
[assertion.2] file divide.adb line 6 Ada Check assertion: SUCCESS
3-
[divide.assertion.1] line 7 assertion C = 2: SUCCESS
2+
[divide.assertion.1] line 6 Ada Check assertion: SUCCESS
3+
[divide.assertion.2] line 7 assertion C = 2: SUCCESS
44
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[assertion.2] file divide_by_zero.adb line 6 Ada Check assertion: FAILURE
2-
[assertion.1] file divide_by_zero.adb line 6 Ada Check assertion: FAILURE
1+
[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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
33
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
44
[p_enum_in.assertion.1] line 19 assertion E in More_Than_Two: SUCCESS
5-
[assertion.1] line 23 Ada Check assertion: SUCCESS
5+
[enum_in.assertion.1] line 23 Ada Check assertion: SUCCESS
66
VERIFICATION SUCCESSFUL

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[assertion.1] file expanded_name.adb line 8 Ada Check assertion: SUCCESS
2-
[expanded_name.assertion.1] line 12 assertion (if Withed_Package.X = 1 then N = 2 else N = 1): SUCCESS
1+
[expanded_name.assertion.1] line 8 Ada Check assertion: SUCCESS
2+
[expanded_name.assertion.2] line 12 assertion (if Withed_Package.X = 1 then N = 2 else N = 1): SUCCESS
33
VERIFICATION SUCCESSFUL

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

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

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
[assertion.1] file floating_definition.adb line 8 Ada Check assertion: SUCCESS
2-
[assertion.2] file floating_definition.adb line 9 Ada Check assertion: SUCCESS
3-
[floating_definition.assertion.1] line 10 assertion Small_Number > 0.9: SUCCESS
4-
[floating_definition.assertion.2] line 11 assertion Large_Number > 22.7: FAILURE
1+
[floating_definition.assertion.1] line 8 Ada Check assertion: SUCCESS
2+
[floating_definition.assertion.4] line 9 Ada Check assertion: SUCCESS
3+
[floating_definition.assertion.2] line 10 assertion Small_Number > 0.9: SUCCESS
4+
[floating_definition.assertion.3] line 11 assertion Large_Number > 22.7: FAILURE
55
VERIFICATION FAILED

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
[floating_point_literals.assertion.1] line 8 assertion X > Z: FAILURE
2-
[floating_point_literals.assertion.2] line 10 assertion X < Z: SUCCESS
3-
[assertion.1] line 12 Ada Check assertion: SUCCESS
4-
[floating_point_literals.assertion.3] line 12 assertion X + Y = Z: FAILURE
5-
[floating_point_literals.assertion.4] line 14 assertion X + Y < Z: SUCCESS
6-
[floating_point_literals.assertion.5] line 16 assertion W < 1.2: SUCCESS
1+
[floating_point_literals.assertion.2] line 8 assertion X > Z: FAILURE
2+
[floating_point_literals.assertion.3] line 10 assertion X < Z: SUCCESS
3+
[floating_point_literals.assertion.1] line 12 Ada Check assertion: SUCCESS
4+
[floating_point_literals.assertion.4] line 12 assertion X + Y = Z: FAILURE
5+
[floating_point_literals.assertion.5] line 14 assertion X + Y < Z: SUCCESS
6+
[floating_point_literals.assertion.6] line 16 assertion W < 1.2: SUCCESS
77
VERIFICATION FAILED

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[assertion.1] file forloop.adb line 6 Ada Check assertion: SUCCESS
2-
[forloop.assertion.1] line 9 assertion A = 6: SUCCESS
1+
[forloop.assertion.1] line 6 Ada Check assertion: SUCCESS
2+
[forloop.assertion.2] line 9 assertion A = 6: SUCCESS
33
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
[assertion.1] file func.adb line 6 Ada Check assertion: SUCCESS
1+
[assign2.assertion.1] line 6 Ada Check assertion: SUCCESS
22
[func.assertion.1] line 10 assertion C = 3: SUCCESS
33
VERIFICATION SUCCESSFUL

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[assertion.1] file func_args.adb line 6 Ada Check assertion: SUCCESS
1+
[assign2.assertion.1] line 6 Ada Check assertion: SUCCESS
22
[func_args.assertion.1] line 10 assertion C = 3: SUCCESS
33
[func_args.assertion.2] line 11 assertion Assign2 (5, 6) = 12: FAILURE
44
VERIFICATION FAILED

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

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

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

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

0 commit comments

Comments
 (0)