From a993327b095ce236c36a4f925dd5be08909cafcb Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 13 Sep 2023 09:39:42 +0200
Subject: [PATCH] Remove optionnal funspec parameter
---
src/kernel_internals/typing/populate_spec.ml | 20 +++++++++++--------
src/kernel_internals/typing/populate_spec.mli | 2 +-
tests/spec/default_spec_mode.ml | 2 +-
3 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 1a03e24a052..b95a56004dd 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -830,11 +830,8 @@ let do_warning kf funspec = function
(* Perform generation of all clauses, adds them to the original specification,
and emit property status for each of them. *)
-let do_populate ?funspec kf clauses =
- let original_spec = match funspec with
- | None -> Annotations.funspec kf
- | Some funspec -> funspec
- in
+let do_populate kf clauses =
+ let original_spec = Annotations.funspec kf in
let config = activated_config kf clauses in
let apply warn_acc get_default mode =
@@ -915,6 +912,7 @@ module Is_populated =
let () = Ast.add_linked_state Is_populated.self
+(* Return the list of clauses not already done for function [kf]. *)
let todo_clauses kf clauses =
let not_populated c = not (Is_populated.mem (kf, c)) in
List.filter not_populated clauses
@@ -927,15 +925,21 @@ let todo_clauses kf clauses =
OR
[do_body] is true
*)
-let populate_funspec ?(do_body=false) ?funspec kf clauses =
+let populate_funspec ?(do_body=false) kf clauses =
let todo = todo_clauses kf clauses in
if todo <> [] then
let has_body = Kernel_function.has_definition kf in
if not has_body || do_body then begin
- do_populate ?funspec kf todo;
+ do_populate kf todo;
List.iter (fun c -> Is_populated.add (kf, c) ()) todo
end
let () =
- let f kf funspec = populate_funspec ~funspec kf [`Assigns]; true in
+ (* This function is deprecated. Until removed, populate assigns and
+ returns true if spec generation was performed. *)
+ let f kf _ =
+ let before = Is_populated.mem (kf, `Assigns) in
+ populate_funspec kf [`Assigns];
+ not before && Is_populated.mem (kf, `Assigns)
+ in
Annotations.populate_spec_ref := f [@@ warning "-3"]
diff --git a/src/kernel_internals/typing/populate_spec.mli b/src/kernel_internals/typing/populate_spec.mli
index 8ece5c2ba43..4df2a0ecedf 100644
--- a/src/kernel_internals/typing/populate_spec.mli
+++ b/src/kernel_internals/typing/populate_spec.mli
@@ -84,4 +84,4 @@ val register :
be generated.
*)
val populate_funspec :
- ?do_body:bool -> ?funspec:funspec -> kernel_function -> clause list -> unit
+ ?do_body:bool -> kernel_function -> clause list -> unit
diff --git a/tests/spec/default_spec_mode.ml b/tests/spec/default_spec_mode.ml
index 14210495d5f..3f3cc661cf0 100644
--- a/tests/spec/default_spec_mode.ml
+++ b/tests/spec/default_spec_mode.ml
@@ -2,7 +2,7 @@ let run () =
let open Populate_spec in
let get_spec kf =
let funspec = Annotations.funspec kf in
- populate_funspec ~do_body:true ~funspec kf [`Exits];
+ populate_funspec ~do_body:true kf [`Exits];
populate_funspec ~do_body:true kf [`Assigns];
populate_funspec ~do_body:true kf [`Requires];
populate_funspec ~do_body:true kf [`Allocates];
--
GitLab