From fccd05adf74dca6ab35e47e68269eeffecb581a0 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Fri, 6 Feb 2026 17:54:49 +0100 Subject: [PATCH] Update warnings about recursive subprograms --- tests/1070__functional_trees_test/test.out | 13 +++++++---- tests/R509-011__higher_order_proof/test.out | 12 ++++++---- .../test.out | 4 +--- .../test.out | 22 +++++++++++++++---- .../test.out | 10 +++------ .../test.out | 14 ++++++++---- .../test.out | 10 +++------ 7 files changed, 52 insertions(+), 33 deletions(-) diff --git a/tests/1070__functional_trees_test/test.out b/tests/1070__functional_trees_test/test.out index ed2cb3aa..9a944f80 100644 --- a/tests/1070__functional_trees_test/test.out +++ b/tests/1070__functional_trees_test/test.out @@ -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] diff --git a/tests/R509-011__higher_order_proof/test.out b/tests/R509-011__higher_order_proof/test.out index 595e2b45..f3ba6a21 100644 --- a/tests/R509-011__higher_order_proof/test.out +++ b/tests/R509-011__higher_order_proof/test.out @@ -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 diff --git a/tests/V818-010__functional_multiset_proof/test.out b/tests/V818-010__functional_multiset_proof/test.out index 21d6f599..14680fdb 100644 --- a/tests/V818-010__functional_multiset_proof/test.out +++ b/tests/V818-010__functional_multiset_proof/test.out @@ -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 diff --git a/tests/W127-011__functional_maps_HO_proof/test.out b/tests/W127-011__functional_maps_HO_proof/test.out index da86725e..21ca5b83 100644 --- a/tests/W127-011__functional_maps_HO_proof/test.out +++ b/tests/W127-011__functional_maps_HO_proof/test.out @@ -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] diff --git a/tests/W127-011__functional_sequences_HO_proof/test.out b/tests/W127-011__functional_sequences_HO_proof/test.out index 766dff80..54dd6168 100644 --- a/tests/W127-011__functional_sequences_HO_proof/test.out +++ b/tests/W127-011__functional_sequences_HO_proof/test.out @@ -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 diff --git a/tests/W127-011__functional_sets_HO_proof/test.out b/tests/W127-011__functional_sets_HO_proof/test.out index 732824ad..80d11300 100644 --- a/tests/W127-011__functional_sets_HO_proof/test.out +++ b/tests/W127-011__functional_sets_HO_proof/test.out @@ -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] diff --git a/tests/W127-011__functional_vectors_HO_proof/test.out b/tests/W127-011__functional_vectors_HO_proof/test.out index 760b0e85..3a679294 100644 --- a/tests/W127-011__functional_vectors_HO_proof/test.out +++ b/tests/W127-011__functional_vectors_HO_proof/test.out @@ -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