diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 76f20f9e9b5ba257584804e1881281bd12c74b09..135c7c0e4aad87d50a2c45e0fd9dca87716ef576 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 4f049e0bf0d288ba0bb7bfbc4069a97ba6f97e0e..dd0e4788566acfa3f01b63666411ace2de1381a4 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 f019256d85fcc2ecc5f633711e8a247e2ca1d099..f2ab22958f088759e106dd9a7474d767698949cd 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 e19abe85b6f1a433061885e34bd0aa74b46fd32e..db61248746275b2710b860f73691fdf50c51fdfe 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} *)