ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Update test outputs

Browse Source
This commit is contained in:
Johannes Kanig
2024-11-22 11:08:13 +09:00
parent 180b11c93b
commit 96c0647d20
5 changed files with 27 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
tests/665__formal_hashed_maps_test/test.out
View File

@@ -439,13 +439,6 @@ test.adb:518:07: info: precondition proved (CVC5: 1 VC)
test.adb:518:46: info: precondition proved (CVC5: 1 VC)
test.adb:522:07: info: initialization of "X" proved
test.adb:522:10: info: initialization of "Y" proved
test.adb:104:07: warning: variable "X" is read but never assigned [-gnatwv]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_maps.ads:244 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_maps.ads:244 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
test.adb:522:19: info: range check proved (CVC5: 2 VC)
test.adb:522:25: info: range check proved (CVC5: 2 VC)
test.adb:525:07: info: precondition proved (CVC5: 1 VC)
@@ -555,3 +548,10 @@ test.adb:653:04: info: precondition proved (Trivial: 1 VC)
test.adb:654:04: info: precondition proved (Trivial: 1 VC)
test.adb:655:04: info: precondition proved (Trivial: 1 VC)
test.adb:656:04: info: precondition proved (Trivial: 1 VC)
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_maps.ads:244 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_maps.ads:244 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
test.adb:104:07: warning: variable "X" is read but never assigned [-gnatwv]

14
tests/665__formal_hashed_sets_test/test.out
View File

@@ -798,13 +798,6 @@ test.adb:882:34: info: precondition proved (CVC5: 1 VC)
test.adb:883:07: info: precondition proved (Z3: 1 VC)
test.adb:887:18: info: elements shall be distinct and shall fit in "Count_Type" for set aggregates at spark-containers-formal-hashed_sets.ads:87, in instantiation at inst.ads:10
test.adb:887:18: info: precondition proved (CVC5: 11 VC)
test.adb:96:07: warning: variable "X" is read but never assigned [-gnatwv]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_sets.ads:291 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_sets.ads:291 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
test.adb:889:07: info: precondition proved (CVC5: 1 VC)
test.adb:890:07: info: precondition proved (CVC5: 1 VC)
test.adb:894:04: info: precondition proved (Trivial: 1 VC)
@@ -854,3 +847,10 @@ test.adb:937:04: info: precondition proved (Trivial: 1 VC)
test.adb:938:04: info: precondition proved (Trivial: 1 VC)
test.adb:939:04: info: precondition proved (Trivial: 1 VC)
test.adb:940:04: info: precondition proved (Trivial: 1 VC)
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_sets.ads:291 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-hashed_sets.ads:291 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
test.adb:96:07: warning: variable "X" is read but never assigned [-gnatwv]

12
tests/665__formal_unbounded_hashed_maps_test/test.out
View File

@@ -288,12 +288,6 @@ test.adb:424:07: medium: precondition might fail
test.adb:425:07: info: precondition proved (Z3: 1 VC)
test.adb:426:07: medium: precondition might fail
test.adb:426:15: info: precondition proved (Z3: 1 VC)
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_maps.ads:236 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_maps.ads:236 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
test.adb:427:07: medium: precondition might fail
test.adb:427:15: info: precondition proved (Z3: 1 VC)
test.adb:432:07: info: precondition proved (Z3: 1 VC)
@@ -437,3 +431,9 @@ test_resize.adb:14:30: info: loop invariant initialization proved (CVC5: 1 VC)
test_resize.adb:14:30: info: loop invariant preservation proved (CVC5: 1 VC)
test_resize.adb:15:30: info: loop invariant initialization proved (CVC5: 2 VC)
test_resize.adb:15:48: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove K in 1 .. I
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_maps.ads:236 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_maps.ads:236 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]

12
tests/665__formal_unbounded_hashed_sets_test/test.out
View File

@@ -655,12 +655,6 @@ test.adb:824:07: info: analyzing call to "Create_Non_Empty_Set_With_Collisions"
test.adb:824:07: info: in inlined body at line 33
test.adb:824:07: info: unrolling loop
test.adb:826:07: info: precondition proved (Z3: 1 VC)
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_sets.ads:278 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_sets.ads:278 [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
test.adb:827:07: medium: precondition might fail
test.adb:831:07: info: initialization of "X" proved
test.adb:831:10: info: initialization of "Y" proved
@@ -746,3 +740,9 @@ test_resize.adb:14:30: info: loop invariant initialization proved (CVC5: 1 VC)
test_resize.adb:14:30: info: loop invariant preservation proved (CVC5: 1 VC)
test_resize.adb:15:30: info: loop invariant initialization proved (CVC5: 2 VC)
test_resize.adb:15:48: medium: loop invariant might not be preserved by an arbitrary iteration, cannot prove K in 1 .. I
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: check will fail at run time [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_sets.ads:278 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-formal-unbounded_hashed_sets.ads:278 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:134 [-gnatw.a]
inst.ads:10:04: warning: in instantiation at spark-containers-functional-maps.ads:153 [-gnatw.a]

2
tests/665__formal_vectors_test/test.out
View File

@@ -1550,7 +1550,6 @@ test_gen.adb:706:04: info: precondition proved (Trivial: 1 VC), in instantiation
test_gen.adb:706:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:14
test_gen.adb:707:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:11
test_gen.adb:707:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:14
test_gen.adb:68:07: warning: variable "X" is read but never assigned [-gnatwv]
test_gen.adb:708:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:11
test_gen.adb:708:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:14
test_gen.adb:709:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:11
@@ -1623,3 +1622,4 @@ test_gen.adb:742:04: info: precondition proved (Trivial: 1 VC), in instantiation
test_gen.adb:742:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:14
test_gen.adb:743:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:11
test_gen.adb:743:04: info: precondition proved (Trivial: 1 VC), in instantiation at test.adb:14
test_gen.adb:68:07: warning: variable "X" is read but never assigned [-gnatwv]