From a9a28c2e7377f52def9aa329d93a9c9673f59efd Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 27 Jul 2023 15:08:58 +0200
Subject: [PATCH] Add an option to turn of generation
---
src/kernel_internals/typing/populate_spec.ml | 13 ++++++-------
src/kernel_services/ast_data/annotations.ml | 3 ++-
src/kernel_services/plugin_entry_points/kernel.ml | 14 ++++++++++++++
src/kernel_services/plugin_entry_points/kernel.mli | 7 ++++---
4 files changed, 26 insertions(+), 11 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 76f20f9e9b5..135c7c0e4aa 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -441,9 +441,8 @@ let get_config_default () =
let get_config () =
let default = get_config_default () in
- let custom_map = Kernel.GeneratedSpecCustom.get () in
- let apply_custom k v conf =
- let mode = get_mode v in
+ let collect (k,v) conf =
+ let mode = get_mode (Option.get v) in
match k with
| "exits" -> {conf with exits = mode}
| "assigns" -> {conf with assigns = mode}
@@ -452,10 +451,10 @@ let get_config () =
| "terminates" -> {conf with terminates = mode}
| s ->
Kernel.abort
- "\'%s\' is not a valid clause for spec generation, accepted \
- values are 'exits', 'assigns', 'allocates' and 'terminates'" s
+ "\'%s\' is not a valid key for -generated-spec-custom, accepted keys \
+ are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'" s
in
- Datatype.String.Map.fold apply_custom custom_map default
+ Kernel.GeneratedSpecCustom.fold collect default
let do_populate kf original_spec =
let config = get_config () in
@@ -500,7 +499,7 @@ module Is_populated =
let () = Ast.add_linked_state Is_populated.self
let populate_funspec kf spec =
- if Is_populated.mem kf then false
+ if not @@ Kernel.GenerateDefaultSpec.get() || Is_populated.mem kf then false
else begin
do_populate kf spec;
Is_populated.add kf ();
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 4f049e0bf0d..dd0e4788566 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -164,7 +164,8 @@ let () =
let populate_spec_ref = Extlib.mk_fun "Annotations.populate_spec"
-let populate_spec populate kf spec = match kf.fundec with
+let populate_spec populate kf spec =
+ match kf.fundec with
| Definition _ -> false
| Declaration _ ->
if populate then begin
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index f019256d85f..f2ab22958f0 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1455,8 +1455,22 @@ module DoCollapseCallCast =
and the lvalue it is assigned to."
end)
+
let () = Parameter_customize.set_group normalisation
let () = Parameter_customize.do_not_reset_on_copy ()
+module GenerateDefaultSpec =
+ Bool
+ (struct
+ let module_name = "GenerateDefaultSpec"
+ let option_name = "-generate-default-spec"
+ let default = true
+ let help = "Generates missing specifications according to options \
+ -generated-spec-mode and -generated-spec-custom (activated \
+ by default)"
+ end)
+let () = Parameter_customize.set_group normalisation
+let () = Parameter_customize.do_not_reset_on_copy ()
+
module GeneratedSpecMode =
String
(struct
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index e19abe85b6f..db612487462 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -556,10 +556,11 @@ module DoCollapseCallCast: Parameter_sig.Bool
This is false by default. Set to true to replicate the behavior
of CIL 1.3.5 and earlier. *)
-
+module GenerateDefaultSpec: Parameter_sig.Bool
module GeneratedSpecMode: Parameter_sig.String
-module GeneratedSpecCustom:
- Parameter_sig.Map with type t = string Datatype.String.Map.t
+module GeneratedSpecCustom: Parameter_sig.Map
+ with type key = string
+ and type value = string
(* ************************************************************************* *)
(** {2 Analysis Behavior of options} *)
--
GitLab