Skip to content

Update tests with ordered properties #330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 22, 2020
Merged

Update tests with ordered properties #330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4005faa
Update tests to have the properties in numeric order
Jan 22, 2020
166a788
Bump lib/cbmc to include diffblue/cbmc#5214
Jan 22, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion lib/cbmc
Open in desktop
Submodule cbmc updated 27 files
+4 −4 .travis.yml
+3 −3 COMPILING.md
+1 −1 buildspec-linux-cmake-gcc-cov.yml
+1 −1 buildspec-linux-cmake-gcc.yml
+1 −1 buildspec-windows-cmake.yml
+1 −1 doc/architectural/compilation-and-development.md
+10 −0 regression/cbmc/incomplete-sizeof/array.c
+9 −0 regression/cbmc/incomplete-sizeof/array.desc
+10 −0 regression/cbmc/incomplete-sizeof/enum.c
+9 −0 regression/cbmc/incomplete-sizeof/enum.desc
+11 −0 regression/cbmc/incomplete-sizeof/struct.c
+9 −0 regression/cbmc/incomplete-sizeof/struct.desc
+10 −0 regression/cbmc/incomplete-sizeof/union.c
+9 −0 regression/cbmc/incomplete-sizeof/union.desc
+15 −0 src/ansi-c/c_typecheck_expr.cpp
+6 −1 src/cpp/cpp_static_assert.h
+11 −6 src/cpp/parse.cpp
+64 −53 src/goto-checker/report_util.cpp
+0 −13 src/util/byte_operators.h
+0 −5 src/util/mathematical_expr.h
+0 −36 src/util/std_code.h
+4 −170 src/util/std_expr.h
+0 −5 src/util/std_types.h
+0 −11 src/util/type.h
+1 −0 unit/Makefile
+102 −0 unit/goto-checker/report_util/is_property_less_than.cpp
+2 −0 unit/goto-checker/report_util/module_dependencies.txt
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/address_clause/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,6 @@ N_Attribute_Definition_Clause "address" (Node_Id=2295) (source,analyzed)
Entity = N_Defining_Identifier "var_addr_2" (Entity_Id=2282)
Check_Address_Alignment = True

[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
[address_clause.assertion.1] line 12 Ada Check assertion: SUCCESS
[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS
VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/arrays_access/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[arrays_access.assertion.1] line 5 Ada Check assertion: SUCCESS
[arrays_access.assertion.2] line 6 assertion Actual7(1) = 2: SUCCESS
Expand Down
28 changes: 14 additions & 14 deletions testsuite/gnat2goto/tests/arrays_assign_nonoverlap/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.14] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.13] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.13] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.14] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.19] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.20] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.21] file <internal> memcpy destination region writeable: SUCCESS
[arrays_assign_nonoverlap.assertion.1] line 8 Ada Check assertion: SUCCESS
[arrays_assign_nonoverlap.assertion.2] line 8 assertion Full_Arr(1)=3: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/arrays_attributes_dynamic/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[array_consumer.assertion.1] line 7 assertion Arr'First = 1: SUCCESS
[array_consumer.assertion.2] line 8 assertion Arr'Last = 1: FAILURE
Expand Down
12 changes: 6 additions & 6 deletions testsuite/gnat2goto/tests/arrays_attributes_static/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
Expand All @@ -16,6 +15,7 @@
[precondition_instance.15] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.16] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.17] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.18] file <internal> memcpy destination region writeable: SUCCESS
[arrays_attributes_static.assertion.1] line 12 Ada Check assertion: SUCCESS
[arrays_attributes_static.assertion.2] line 16 assertion Array_Attribs = 41: SUCCESS
[arrays_attributes_static.assertion.3] line 17 assertion An_Index = 12: SUCCESS
Expand Down
10 changes: 5 additions & 5 deletions testsuite/gnat2goto/tests/arrays_concat/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.10] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.11] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.12] file <internal> memcpy destination region writeable: SUCCESS
[arrays_concat.assertion.1] line 7 Ada Check assertion: SUCCESS
[arrays_concat.assertion.2] line 7 assertion Actual(2)=4: SUCCESS
VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/arrays_constraints/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[array_constraints.assertion.1] line 109 Ada Check assertion: SUCCESS
[array_constraints.assertion.8] line 117 Ada Check assertion: SUCCESS
[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
[array_constraints.assertion.8] line 117 Ada Check assertion: SUCCESS
[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
[array_constraints.assertion.4] line 143 assertion VEA1 (One) + VEA2 (Two) + VEA3 (Three) + VEA4 (Four) + VEA5 (Five) + VEA6 (Six) = 21: SUCCESS
[array_constraints.assertion.5] line 154 assertion VBA1 (False) + VBA2 (True) + VBA3 (False) + VBA4 (True) + VBA5 (False) + VBA6 (True) = 7: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/arrays_index/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[arrays_index.assertion.1] line 5 Ada Check assertion: SUCCESS
[arrays_index.assertion.2] line 9 assertion Actual(2) = 11: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/arrays_index_enum/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[test.assertion.1] line 7 Ada Check assertion: SUCCESS
[test.assertion.2] line 7 assertion Array_Value(Two) = 2: SUCCESS
Expand Down
4 changes: 2 additions & 2 deletions testsuite/gnat2goto/tests/arrays_range/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[array_consumer.assertion.1] line 8 Ada Check assertion: SUCCESS
[array_consumer.assertion.2] line 8 Ada Check assertion: FAILURE
[array_consumer.assertion.3] line 9 assertion An_Index = 2: SUCCESS
[array_consumer.assertion.4] line 11 assertion An_Index = 4: SUCCESS
[array_consumer.assertion.5] line 13 assertion An_Index = -1: SUCCESS
Expand Down
4 changes: 2 additions & 2 deletions testsuite/gnat2goto/tests/arrays_write_element/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[arrays_write_element.assertion.1] line 6 Ada Check assertion: SUCCESS
VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/attrib_address/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
VERIFICATION SUCCESSFUL
4 changes: 2 additions & 2 deletions testsuite/gnat2goto/tests/enum_in_param/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[enum_in.assertion.1] line 23 Ada Check assertion: SUCCESS
[p_enum_in.assertion.1] line 19 assertion E in More_Than_Two: SUCCESS
VERIFICATION SUCCESSFUL
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/expanded_name_subtype_indication/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[test.assertion.2] line 8 assertion Val < 2.0: SUCCESS
[test.assertion.3] line 10 assertion Val > 0.0: SUCCESS
[test.assertion.4] line 11 assertion Val * 20.0 < 10.0: FAILURE
[test.assertion.1] line 11 Ada Check assertion: SUCCESS
[test.assertion.4] line 11 assertion Val * 20.0 < 10.0: FAILURE
VERIFICATION FAILED
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/if_integer/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[assertion.1] file divide.adb line 4 Ada Check assertion: SUCCESS
[divide.assertion.2] line 4 assertion B / 1 = B: SUCCESS
[divide.assertion.3] line 6 assertion B / B = 1: SUCCESS
[divide.assertion.1] line 6 Ada Check assertion: SUCCESS
[divide.assertion.3] line 6 assertion B / B = 1: SUCCESS
[divide.assertion.4] line 8 assertion B < 0: FAILURE
VERIFICATION FAILED
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/in_expression/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[in_expression.assertion.1] line 8 assertion Val < 1: FAILURE
[in_expression.assertion.2] line 10 assertion Val > 1: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/index_check/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[main.assertion.2] line 6 Ada Check assertion: FAILURE
[main.assertion.1] line 9 assertion AnArray(3)=6: SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion testsuite/gnat2goto/tests/package_type/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[package_type.assertion.2] line 8 assertion Small_Number * 2 = 8: SUCCESS
[package_type.assertion.1] line 8 Ada Check assertion: SUCCESS
[package_type.assertion.2] line 8 assertion Small_Number * 2 = 8: SUCCESS
VERIFICATION SUCCESSFUL
4 changes: 2 additions & 2 deletions testsuite/gnat2goto/tests/representation_clause_component_size/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[test.assertion.1] line 16 assertion My_Storage_Array(2)=2: SUCCESS
VERIFICATION SUCCESSFUL
14 changes: 7 additions & 7 deletions testsuite/gnat2goto/tests/rhs_array_assign/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
[rhs_array_assign.assertion.1] line 8 Ada Check assertion: SUCCESS
[rhs_array_assign.assertion.2] line 9 assertion A (5) = 5 and A (1) = 0: SUCCESS
VERIFICATION SUCCESSFUL