Mode Skip is available in -generated-spec-custom option

src/kernel_internals/typing/populate_spec.ml

@@ -23,9 +23,11 @@
 open Cil_types
 
 type mode =
-  | ACSL | Safe | Frama_C (* Modes available for specification generation. *)
-  | Skip (* Internally used to skip generation. *)
-  | Other of string (* Allow user to use a custom mode, see {!register}. *)
+  (* Modes available for specification generation. Skip is only available via
+     -generated-spec-custom (cf. option description). *)
+  | ACSL | Safe | Frama_C | Skip
+  (* Allow user to use a custom mode, see {!register}. *)
+  | Other of string
 
 (* Allow customization, each clause can be handled with a different {!mode}. *)
 type config = {
@@ -733,10 +735,16 @@ module Allocates = Make(Allocates_generator)
 module Terminates = Make(Terminates_generator)
 
 (* Convert string from parameter [-generated-spec-mode] to [mode]. *)
-let get_mode = function
+let get_mode ~allow_skip = function
   | "frama-c" -> Frama_C
   | "acsl" -> ACSL
   | "safe" -> Safe
+  | "skip" when allow_skip -> Skip
+  | "skip" ->
+    Kernel.warning ~once:true
+      "Mode skip is only available via -generated-spec-custom.@, The mode \
+       frama-c will be used instead";
+    Frama_C
   | s -> Other s
 
 (* Given a [mode], returns the configuration for each clause. *)
@@ -751,14 +759,14 @@ let build_config mode =
 
 (* Build configuration from parameter [-generated-spec-mode]. *)
 let get_config_mode () =
-  Kernel.GeneratedSpecMode.get () |> get_mode |> build_config
+  Kernel.GeneratedSpecMode.get () |> get_mode ~allow_skip:false |> build_config
 
 (* Build the default configuration, then select modes depending on the
    parameter [-generated-spec-custom]. *)
 let get_config_custom () =
   let default = get_config_mode () in
   let collect (k,v) config =
-    let mode = get_mode (Option.get v) in
+    let mode = get_mode ~allow_skip:true (Option.get v) in
     match k with
     | "exits" -> {config with c_exits = mode}
     | "assigns" -> {config with c_assigns = mode}

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1486,8 +1486,11 @@ module GeneratedSpecCustom =
       let arg_name = "c1:m1,c2:m2,..."
       let default = Datatype.String.Map.empty
       let help =
-        "Fine-tune missing specification generation by manually choosing \
-         modes for each clause. See user manual for more information."
+        "Fine-tune missing specification generation by manually selecting \
+         modes for each clause. Can be one of: frama-c, acsl, safe, skip or \
+         the name of a custom registered mode. Do not use skip mode for \
+         assigns unless you know what you are doing! See user manual for more \
+         information."
     end)
 
 let normalization_parameters () =

tests/spec/default_spec_mode.i

@@ -3,8 +3,8 @@
    STDOPT: +"-generated-spec-mode acsl"
    STDOPT: +"-generated-spec-mode safe"
    STDOPT: +"-generated-spec-mode frama-c"
-   STDOPT: +"-generated-spec-custom exits:acsl,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
-
+   STDOPT: +"-generated-spec-mode skip"
+   STDOPT: +"-generated-spec-custom exits:skip,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
    EXIT: 1
    STDOPT: +"-generated-spec-custom wrong_clause:safe"
    STDOPT: +"-generated-spec-custom wrong_clause:"

tests/spec/oracle/default_spec_mode.3.res.oracle

 [kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] Warning: Mode skip is only available via -generated-spec-custom.
+   The mode frama-c will be used instead
 [kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
   Neither code nor specification for function f1,
    generating default exits. See -generated-spec-* options for more info
@@ -6,7 +8,7 @@
   Neither code nor explicit assigns for function f1,
    generating default clauses. See -generated-spec-* options for more info
 [kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
-  Neither code nor explicit requires for function f1,
+  Neither code nor explicit allocates for function f1,
    generating default clauses. See -generated-spec-* options for more info
 [kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
   Neither code nor explicit terminates for function f1,
@@ -17,14 +19,17 @@
 [kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
   Neither code nor explicit assigns for function f3,
    generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor explicit allocates for function f3,
+   generating default clauses. See -generated-spec-* options for more info
 [kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
   Neither code nor explicit terminates for function f3,
    generating default clauses. See -generated-spec-* options for more info
 /* Generated by Frama-C */
-/*@ requires \false;
-    terminates \true;
+/*@ terminates \true;
     exits \false;
-    assigns \nothing; */
+    assigns \nothing;
+    allocates \nothing; */
 void f1(void);
 
 /*@ terminates \true;
@@ -43,6 +48,7 @@ void f2(void)
     assigns \result, *a;
     assigns \result \from *a;
     assigns *a \from *a;
+    allocates \nothing;
  */
 int f3(int *a);
 

tests/spec/oracle/default_spec_mode.4.res.oracle

 [kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
-   Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
-[kernel] Frama-C aborted: invalid user input.
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor specification for function f1,
+   generating default assigns. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor explicit requires for function f1,
+   generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor explicit terminates for function f1,
+   generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor explicit assigns for function f3,
+   generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning: 
+  Neither code nor explicit terminates for function f3,
+   generating default clauses. See -generated-spec-* options for more info
+/* Generated by Frama-C */
+/*@ requires \false;
+    terminates \true;
+    assigns \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+    assigns \nothing;
+    allocates \nothing; */
+void f2(void)
+{
+  f1();
+  return;
+}
+
+/*@ requires \true;
+    terminates \true;
+    assigns \result, *a;
+    assigns \result \from *a;
+    assigns *a \from *a;
+ */
+int f3(int *a);
+
+/*@ requires \true;
+    terminates \true;
+    assigns *b;
+    allocates \nothing; */
+int f4(int *b)
+{
+  int tmp;
+  tmp = f3(b);
+  return tmp;
+}
+
+

tests/spec/oracle/default_spec_mode.6.res.oracle

+[kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+   Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+[kernel] Frama-C aborted: invalid user input.