diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml index 135c7c0e4aad87d50a2c45e0fd9dca87716ef576..75919e8eda863a39ca6a94f102a0c8a1c3ffbe28 100644 --- a/src/kernel_internals/typing/populate_spec.ml +++ b/src/kernel_internals/typing/populate_spec.ml @@ -22,7 +22,7 @@ open Cil_types -type mode = ACSL | Safe | Frama_C | Other of string +type mode = ACSL | Safe | Frama_C | Skip | Other of string [@@ warning "-37"] (* TODO: to build Other value *) type config = { @@ -77,7 +77,7 @@ module Make(G : Generator) = struct let get_default mode kf spec = let table = G.collect_behaviors spec in - if G.has_behavior default table then + if mode = Skip || G.has_behavior default table then Kept else if mode = ACSL then Generated (G.acsl_default ()) @@ -91,7 +91,7 @@ struct Generated(G.frama_c_default kf) | None -> match mode with - | ACSL | Safe | Frama_C -> assert false + | ACSL | Safe | Frama_C | Skip -> assert false | Other mode -> Generated(G.custom_default mode kf spec) @@ -154,7 +154,7 @@ struct | Generated exits -> match mode with | Frama_C -> emit_status kf bhv exits Property_status.Dont_know - | ACSL | Safe | Other _ -> () + | Skip | ACSL | Safe | Other _ -> () end @@ -245,7 +245,7 @@ struct | Generated assigns -> match mode with | Frama_C -> emit_status kf bhv assigns Property_status.Dont_know - | ACSL | Safe | Other _ -> () + | ACSL | Safe | Skip | Other _ -> () end @@ -358,7 +358,7 @@ struct emit_status kf bhv allocates Property_status.True | Frama_C -> emit_status kf bhv allocates Property_status.Dont_know - | Other _ | Safe -> () + | Other _ | Safe | Skip -> () end @@ -409,7 +409,7 @@ struct emit_status kf bhv terminates Property_status.True | Safe | Frama_C -> emit_status kf bhv terminates Property_status.Dont_know - | Other _ -> () + | Skip | Other _ -> () end @@ -423,10 +423,12 @@ let get_mode = function | "frama-c" -> Frama_C | "acsl" -> ACSL | "safe" -> Safe + | "skip" -> Skip | s -> + (* TODO: to build Other value *) Kernel.abort - "\'%s\' is not a valid mode for spec generation, accepted values \ - are 'frama-c', 'acsl' and 'safe'" s + "@[@['%s'@] is not a supported mode for -generated-spec-mode.@ Accepted \ + keys are 'acsl', 'frama-c', 'safe' and 'skip'.@]@." s let build_config mode = { exits = mode; @@ -451,8 +453,9 @@ let get_config () = | "terminates" -> {conf with terminates = mode} | s -> Kernel.abort - "\'%s\' is not a valid key for -generated-spec-custom, accepted keys \ - are 'exits', 'assigns', 'requires', '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 Kernel.GeneratedSpecCustom.fold collect default diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index f2ab22958f088759e106dd9a7474d767698949cd..4283c3bd919d3265b3cebee0ed06a58289d8f7fd 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1482,7 +1482,6 @@ module GeneratedSpecMode = "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 () @@ -1496,7 +1495,7 @@ module GeneratedSpecCustom = end) (struct let option_name = "-generated-spec-custom" - let arg_name = "exits|assigns|allocates|terminates:frama-c|acsl|safe" + let arg_name = "c1:m1,c2:m2,..." let default = Datatype.String.Map.empty let help = "Fine-tune missing specs configuration by manually choosing modes for\