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

Merge branch 'topic/1187-dross-proof-cyclic' into 'master'

Browse Source 
Update warnings about recursive subprograms

Issue: eng/spark/spark2014#1187

See merge request eng/spark/sparklib!234
This commit is contained in:
Claire Dross
2026-02-10 09:28:51 +00:00
parent ca214c2cc4 fccd05adf7
commit 7e9d23fdd4
7 changed files with 52 additions and 33 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
tests/1070__functional_trees_test/test.out
View File

@@ -1,7 +1,7 @@
test.adb:19:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test.adb:19:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test.adb:19:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test.adb:19:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test.adb:19:04: warning: "=" is recursive; its contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test.adb:19:04: warning: "Count" is recursive; (implicit) contract of mutally recursive functions might not be available on calls from contracts and assertions [contracts-recursive]
test.adb:19:04: warning: "Count_Children" is recursive; (implicit) contract of mutally recursive functions might not be available on calls from contracts and assertions [contracts-recursive]
test.adb:19:04: warning: "Height" is recursive; its contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:105
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:113
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:125
@@ -9,6 +9,11 @@ test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.a
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:233
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:78
test.adb:19:04: warning: in instantiation at spark-containers-functional-trees.ads:97
test.adb:19:04: warning: its contract might be missing
test.adb:19:04: warning: its contract might be missing
test.adb:19:04: warning: potentially missing automatically instanciated lemma "Lemma_Count_Children_Tail" declared at spark-containers-functional-trees.ads:249, instance at line 19
test.adb:19:04: warning: potentially missing contract for "Count" declared at spark-containers-functional-trees.ads:140, instance at line 19
test.adb:19:04: warning: potentially missing contract for "Count_Children" declared at spark-containers-functional-trees.ads:233, instance at line 19
test.adb:19:04: warning: precondition is statically False [precondition-statically-false]
test.adb:19:04: warning: precondition is statically False [precondition-statically-false]
test.adb:19:04: warning: precondition is statically False [precondition-statically-false]

12
tests/R509-011__higher_order_proof/test.out
View File

@@ -2268,10 +2268,11 @@ test_higher_order2.adb:13:17: info: overflow check proved
test_higher_order2.adb:20:24: info: precondition proved
test_higher_order2.ads:38:13: info: implicit aspect Always_Terminates on "Valid_Integer" has been proved, subprogram will terminate
test_higher_order2.ads:39:17: info: predicate check proved
test_higher_order2.ads:43:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_higher_order2.ads:43:04: warning: "No_Overflows" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_higher_order2.ads:43:04: warning: in instantiation at spark-higher_order-fold.adb:508
test_higher_order2.ads:43:04: warning: in instantiation at spark-higher_order-fold.ads:364
test_higher_order2.ads:43:04: warning: in instantiation at spark-higher_order-fold.ads:404
test_higher_order2.ads:43:04: warning: in instantiation at spark-higher_order-fold.ads:404
test_higher_order2.ads:43:04: warning: in instantiation at spark-higher_order-fold.ads:91
test_higher_order2.ads:43:04: warning: initialization of an array in FOR loop is handled imprecisely [array-initialization]
test_higher_order2.ads:56:06: info: data dependencies proved
@@ -2279,10 +2280,11 @@ test_higher_order2.ads:57:14: info: postcondition proved
test_higher_order2.ads:59:13: info: implicit aspect Always_Terminates on "Sum_Int" has been proved, subprogram will terminate
test_higher_order2.ads:60:14: info: postcondition proved
test_higher_order2.ads:61:34: info: predicate check proved
test_higher_order2.ads:86:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_higher_order2.ads:86:04: warning: "No_Overflows" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_higher_order2.ads:86:04: warning: in instantiation at spark-higher_order-fold.adb:508
test_higher_order2.ads:86:04: warning: in instantiation at spark-higher_order-fold.ads:364
test_higher_order2.ads:86:04: warning: in instantiation at spark-higher_order-fold.ads:404
test_higher_order2.ads:86:04: warning: in instantiation at spark-higher_order-fold.ads:404
test_higher_order2.ads:86:04: warning: in instantiation at spark-higher_order-fold.ads:91
test_higher_order2.ads:86:04: warning: initialization of an array in FOR loop is handled imprecisely [array-initialization]
test_higher_order2.ads:104:04: warning: in instantiation at spark-higher_order-fold.adb:595
@@ -2336,22 +2338,24 @@ test_higher_order3.ads:22:04: warning: in instantiation at spark-higher_order-fo
test_higher_order3.ads:22:04: warning: initialization of an array in FOR loop is handled imprecisely [array-initialization]
test_higher_order3.ads:28:13: info: implicit aspect Always_Terminates on "Valid_Integer" has been proved, subprogram will terminate
test_higher_order3.ads:29:17: info: predicate check proved
test_higher_order3.ads:33:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_higher_order3.ads:33:04: warning: "No_Overflows" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_higher_order3.ads:33:04: warning: in instantiation at spark-higher_order-fold.adb:415
test_higher_order3.ads:33:04: warning: in instantiation at spark-higher_order-fold.ads:617
test_higher_order3.ads:33:04: warning: in instantiation at spark-higher_order-fold.ads:706
test_higher_order3.ads:33:04: warning: in instantiation at spark-higher_order-fold.ads:760
test_higher_order3.ads:33:04: warning: in instantiation at spark-higher_order-fold.ads:760
test_higher_order3.ads:33:04: warning: initialization of a multi-dimensional array in nested FOR loops is handled imprecisely [multidimensional-array-init]
test_higher_order3.ads:47:06: info: data dependencies proved
test_higher_order3.ads:48:14: info: postcondition proved
test_higher_order3.ads:50:13: info: implicit aspect Always_Terminates on "Sum_Int" has been proved, subprogram will terminate
test_higher_order3.ads:51:14: info: postcondition proved
test_higher_order3.ads:52:34: info: predicate check proved
test_higher_order3.ads:77:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_higher_order3.ads:77:04: warning: "No_Overflows" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_higher_order3.ads:77:04: warning: in instantiation at spark-higher_order-fold.adb:415
test_higher_order3.ads:77:04: warning: in instantiation at spark-higher_order-fold.ads:617
test_higher_order3.ads:77:04: warning: in instantiation at spark-higher_order-fold.ads:706
test_higher_order3.ads:77:04: warning: in instantiation at spark-higher_order-fold.ads:760
test_higher_order3.ads:77:04: warning: in instantiation at spark-higher_order-fold.ads:760
test_higher_order3.ads:77:04: warning: initialization of a multi-dimensional array in nested FOR loops is handled imprecisely [multidimensional-array-init]
test_higher_order3.ads:89:04: warning: in instantiation at spark-higher_order-fold.adb:415
test_higher_order3.ads:89:04: warning: in instantiation at spark-higher_order-fold.ads:617

4
tests/V818-010__functional_multiset_proof/test.out
View File

@@ -1,6 +1,4 @@
my_multiset.ads:6:01: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
my_multiset.ads:6:01: warning: function contract might not be available on recursive calls [contracts-recursive]
my_multiset.ads:6:01: warning: in instantiation at spark-containers-functional-multisets.adb:17
my_multiset.ads:6:01: warning: "Cardinality_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
my_multiset.ads:6:01: warning: in instantiation at spark-containers-functional-multisets.adb:17
spark-containers-functional-maps.ads:36:16: info: aspect Always_Terminates on "Eq_Reflexive" has been proved, subprogram will terminate, in instantiation at spark-containers-functional-multisets.ads:580, in instantiation at my_multiset.ads:6
spark-containers-functional-maps.ads:39:16: info: aspect Always_Terminates on "Eq_Symmetric" has been proved, subprogram will terminate, in instantiation at spark-containers-functional-multisets.ads:580, in instantiation at my_multiset.ads:6

22
tests/W127-011__functional_maps_HO_proof/test.out
View File

@@ -542,9 +542,23 @@ test_map_ho.adb:67:04: info: in instantiation at spark-containers-functional-map
test_map_ho.adb:67:04: info: in instantiation at spark-containers-functional-maps-higher_order.adb:328
test_map_ho.adb:67:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_map_ho.adb:67:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_map_ho.adb:67:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_map_ho.adb:67:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_map_ho.adb:67:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:17
test_map_ho.adb:67:04: warning: "Count_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_map_ho.adb:67:04: warning: "Sum_Rec" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:17
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:28
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:43
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:60
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:71
test_map_ho.adb:67:04: warning: in instantiation at spark-containers-functional-maps-higher_order.adb:86
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Count_Eq" declared at spark-containers-functional-maps-higher_order.ads:151, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Count_Eq" declared at spark-containers-functional-maps-higher_order.ads:151, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Count_Remove" declared at spark-containers-functional-maps-higher_order.ads:169, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Count_Remove" declared at spark-containers-functional-maps-higher_order.ads:169, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Eq" declared at spark-containers-functional-maps-higher_order.ads:254, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Eq" declared at spark-containers-functional-maps-higher_order.ads:254, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Remove" declared at spark-containers-functional-maps-higher_order.ads:273, instance at line 67
test_map_ho.adb:67:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Remove" declared at spark-containers-functional-maps-higher_order.ads:273, instance at line 67
test_map_ho.adb:67:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]
test_map_ho.adb:67:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]
test_map_ho.adb:67:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]
test_map_ho.adb:67:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]

10
tests/W127-011__functional_sequences_HO_proof/test.out
View File

@@ -578,13 +578,9 @@ test_sequence_ho.adb:47:04: info: local subprogram "Do_Proof" only analyzed in t
test_sequence_ho.adb:47:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:47:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:47:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:47:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:47:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:47:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:47:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_sequence_ho.adb:47:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_sequence_ho.adb:47:04: warning: "Count_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:47:04: warning: "Filter_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:47:04: warning: "Sum_Rec" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:47:04: warning: in instantiation at spark-containers-functional-infinite_sequences-higher_order.adb:13
test_sequence_ho.adb:47:04: warning: in instantiation at spark-containers-functional-infinite_sequences-higher_order.adb:13
test_sequence_ho.adb:47:04: warning: in instantiation at spark-containers-functional-infinite_sequences-higher_order.adb:25
test_sequence_ho.adb:47:04: warning: in instantiation at spark-containers-functional-infinite_sequences-higher_order.adb:25
test_sequence_ho.adb:47:04: warning: in instantiation at spark-containers-functional-infinite_sequences-higher_order.adb:39

14
tests/W127-011__functional_sets_HO_proof/test.out
View File

@@ -537,9 +537,15 @@ test_set_ho.adb:49:04: info: in instantiation at spark-containers-functional-set
test_set_ho.adb:49:04: info: in instantiation at spark-containers-functional-sets-higher_order.adb:363
test_set_ho.adb:49:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_set_ho.adb:49:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_set_ho.adb:49:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_set_ho.adb:49:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_set_ho.adb:49:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_set_ho.adb:49:04: warning: in instantiation at spark-containers-functional-sets-higher_order.adb:43
test_set_ho.adb:49:04: warning: "Count_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_set_ho.adb:49:04: warning: "Sum_Rec" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_set_ho.adb:49:04: warning: in instantiation at spark-containers-functional-sets-higher_order.adb:43
test_set_ho.adb:49:04: warning: in instantiation at spark-containers-functional-sets-higher_order.adb:78
test_set_ho.adb:49:04: warning: in instantiation at spark-containers-functional-sets-higher_order.adb:85
test_set_ho.adb:49:04: warning: in instantiation at spark-containers-functional-sets-higher_order.adb:95
test_set_ho.adb:49:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Eq" declared at spark-containers-functional-sets-higher_order.ads:300, instance at line 49
test_set_ho.adb:49:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Eq" declared at spark-containers-functional-sets-higher_order.ads:300, instance at line 49
test_set_ho.adb:49:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Remove" declared at spark-containers-functional-sets-higher_order.ads:314, instance at line 49
test_set_ho.adb:49:04: warning: potentially missing automatically instanciated lemma "Lemma_Sum_Remove" declared at spark-containers-functional-sets-higher_order.ads:314, instance at line 49
test_set_ho.adb:49:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]
test_set_ho.adb:49:04: warning: references between entities introduce a cycle in proof dependencies; (implicit) contract of mutally dependent functions might not be available on calls from contracts and assertions [cyclic-dependency]

10
tests/W127-011__functional_vectors_HO_proof/test.out
View File

@@ -504,13 +504,9 @@ test_sequence_ho.adb:61:04: info: local subprogram "Do_Proof" only analyzed in t
test_sequence_ho.adb:61:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:61:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:61:04: info: local subprogram "Do_Proof" only analyzed in the context of calls [info-unrolling-inlining]
test_sequence_ho.adb:61:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:61:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:61:04: warning: expression function body of subprograms with a numeric variant might not be available on recursive calls [numeric-variant]
test_sequence_ho.adb:61:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_sequence_ho.adb:61:04: warning: function contract might not be available on recursive calls [contracts-recursive]
test_sequence_ho.adb:61:04: warning: "Count_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:61:04: warning: "Filter_Rec" is recursive; its body and contract might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:61:04: warning: "Sum_Rec" is recursive; its body might not be available on recursive calls from contracts and assertions [contracts-recursive]
test_sequence_ho.adb:61:04: warning: in instantiation at spark-containers-functional-vectors-higher_order.adb:13
test_sequence_ho.adb:61:04: warning: in instantiation at spark-containers-functional-vectors-higher_order.adb:13
test_sequence_ho.adb:61:04: warning: in instantiation at spark-containers-functional-vectors-higher_order.adb:26
test_sequence_ho.adb:61:04: warning: in instantiation at spark-containers-functional-vectors-higher_order.adb:26
test_sequence_ho.adb:61:04: warning: in instantiation at spark-containers-functional-vectors-higher_order.adb:40