diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 96a87f76105ae1c1afc382f32e24f6d311771bd4..56675009be069749072c087a0ca5d61e10f02560 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -23,6 +23,15 @@
open Cil_types
type mode = ACSL | Safe | Frama_C | Other of string
+[@@ warning "-37"] (* TODO: to build Other value *)
+
+type config = {
+ exits: mode;
+ assigns: mode;
+ allocates: mode;
+ terminates: mode;
+}
+
type 'a result = Kept | Generated of 'a
let default = Cil.default_behavior_name
@@ -68,39 +77,6 @@ struct
Generated(G.custom_default mode kf spec)
end
-module Terminates_generator =
-struct
-
- type clause = identified_predicate option
- type behaviors = bool
-
- let has_behavior name behaviors =
- if name = default then behaviors else false
-
- let collect_behaviors spec =
- None <> spec.spec_terminates
-
- let completes _ _ = None
-
- let acsl_default () =
- Some(Logic_const.(new_predicate ptrue))
-
- let safe_default has_body =
- if has_body
- then Some(Logic_const.(new_predicate ptrue))
- else Some(Logic_const.(new_predicate pfalse))
-
- let frama_c_default () =
- acsl_default ()
-
- let combine_default _ =
- acsl_default ()
-
- let custom_default _mode _kf _spec =
- acsl_default ()
-
-end
-
module Exits_generator =
struct
@@ -226,7 +202,7 @@ struct
end
-module Allocation_generator =
+module Allocates_generator =
struct
type clause = allocation
type behaviors = (string, allocation) Hashtbl.t
@@ -284,20 +260,87 @@ struct
end
-module Terminates = Make(Terminates_generator)
+module Terminates_generator =
+struct
+
+ type clause = identified_predicate option
+ type behaviors = bool
+
+ let has_behavior name behaviors =
+ if name = default then behaviors else false
+
+ let collect_behaviors spec =
+ None <> spec.spec_terminates
+
+ let completes _ _ = None
+
+ let acsl_default () =
+ Some(Logic_const.(new_predicate ptrue))
+
+ let safe_default has_body =
+ if has_body
+ then Some(Logic_const.(new_predicate ptrue))
+ else Some(Logic_const.(new_predicate pfalse))
+
+ let frama_c_default () =
+ acsl_default ()
+
+ let combine_default _ =
+ acsl_default ()
+
+ let custom_default _mode _kf _spec =
+ acsl_default ()
+
+end
+
module Exits = Make(Exits_generator)
module Assigns = Make(Assigns_generator)
-module Allocation = Make(Allocation_generator)
+module Allocates = Make(Allocates_generator)
+module Terminates = Make(Terminates_generator)
let emitter = Emitter.create "gen" [ Funspec ] ~correctness:[] ~tuning:[]
+let get_mode = function
+ | "frama-c" -> Frama_C
+ | "acsl" -> ACSL
+ | "safe" -> Safe
+ | s ->
+ Kernel.abort "\'%s\' is not a valid mode for spec generation, accepted values \
+ are 'frama-c', 'acsl' and 'safe'" s
+
+let build_config mode = {
+ exits = mode;
+ assigns = mode;
+ allocates = mode;
+ terminates = mode;
+}
+
+let get_config_default () =
+ build_config @@ get_mode @@ Kernel.GeneratedSpecMode.get ()
+
+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
+ match k with
+ | "exits" -> {conf with exits = mode}
+ | "assigns" -> {conf with assigns = mode}
+ | "allocates" -> {conf with allocates = mode}
+ | "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
+ in
+ Datatype.String.Map.fold apply_custom custom_map default
+
let do_populate kf original_spec =
- let mode = Frama_C in
+ let config = get_config () in
- let exits = Exits.get_default mode kf original_spec in
- let assigns = Assigns.get_default mode kf original_spec in
- let allocation = Allocation.get_default mode kf original_spec in
- let terminates = Terminates.get_default mode kf original_spec in
+ let exits = Exits.get_default config.exits kf original_spec in
+ let assigns = Assigns.get_default config.assigns kf original_spec in
+ let allocates = Allocates.get_default config.allocates kf original_spec in
+ let terminates = Terminates.get_default config.terminates kf original_spec in
let generated original = function
| Kept -> original
@@ -307,7 +350,7 @@ let do_populate kf original_spec =
let bhv = Cil.mk_behavior () in
let bhv = { bhv with b_post_cond = generated bhv.b_post_cond exits } in
let bhv = { bhv with b_assigns = generated bhv.b_assigns assigns } in
- let bhv = { bhv with b_allocation = generated bhv.b_allocation allocation } in
+ let bhv = { bhv with b_allocation = generated bhv.b_allocation allocates } in
let spec = Cil.empty_funspec () in
let spec = { spec with spec_behavior = [ bhv ] } in
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d7b572fffdd8a956478b1aff071702beb9f9abb4..f019256d85fcc2ecc5f633711e8a247e2ca1d099 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1455,6 +1455,40 @@ 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 GeneratedSpecMode =
+ String
+ (struct
+ let module_name = "GeneratedSpecMode"
+ let option_name = "-generated-spec-mode"
+ let default = "frama-c"
+ let arg_name = "mode"
+ let help =
+ "Select which mode will be used to generate missing specs \
+ (defaults to frama-c), see user manual for more informations"
+ end)
+let () = GeneratedSpecMode.set_possible_values ["frama-c"; "acsl"; "safe"]
+
+let () = Parameter_customize.set_group normalisation
+let () = Parameter_customize.do_not_reset_on_copy ()
+module GeneratedSpecCustom =
+ P.String_map
+ (struct
+ include Datatype.String
+ type key = string
+ let of_string ~key:_ ~prev:_ s = s
+ let to_string ~key:_ s = s
+ end)
+ (struct
+ let option_name = "-generated-spec-custom"
+ let arg_name = "exits|assigns|allocates|terminates:frama-c|acsl|safe"
+ let default = Datatype.String.Map.empty
+ let help =
+ "Fine-tune missing specs configuration by manually choosing modes for\
+ each clause, see user manual for more informations"
+ end)
+
let normalization_parameters () =
let norm = Cmdline.Group.name normalisation in
let kernel = Plugin.get_from_name "" in
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 0d3698e07a0ba10787cca970dd90d472c25179c5..e19abe85b6f1a433061885e34bd0aa74b46fd32e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -556,6 +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 GeneratedSpecMode: Parameter_sig.String
+module GeneratedSpecCustom:
+ Parameter_sig.Map with type t = string Datatype.String.Map.t
+
(* ************************************************************************* *)
(** {2 Analysis Behavior of options} *)
(* ************************************************************************* *)