[Kernel] extend -permissive to include unknown options

src/kernel_services/cmdline_parameters/cmdline.ml

@@ -76,6 +76,7 @@ let journal_isset_ref = ref false
 let use_obj_ref = ref true
 let use_type_ref = ref true
 let deterministic = ref false
+let permissive = ref false
 
 let last_project_created_by_copy = ref (fun () -> assert false)
 
@@ -268,6 +269,11 @@ let error name msg =
     "option `%s' %s.@\nuse `%s -help' for more information."
     name msg bin_name
 
+let warning name msg =
+  Kernel_log.warning
+    "option `%s' %s, ignoring. [-permissive]@\n"
+    name msg
+
 let all_options = match Array.to_list Sys.argv with
   | [] -> assert false
   | _binary :: l -> l
@@ -343,6 +349,9 @@ let parse known_options_list then_expected options_list =
         unknown_options, nb_used, Some (then_options, Replace)
     | "-then-on" :: project_name :: then_options when then_expected ->
         unknown_options, nb_used, Some (then_options, Name project_name)
+    | "-permissive" :: next_options ->
+      permissive := true;
+      go unknown_options nb_used next_options
     | option :: (arg :: next_options as arg_next) ->
         let unknown, use_arg, is_used =
           parse_one_option unknown_options option arg
@@ -386,6 +395,7 @@ let () =
         "-kernel-verbose", Int (fun n -> Kernel_verbose_level.set n);
         "-kernel-debug", Int (fun n -> Kernel_debug_level.set n);
         "-deterministic", Unit (fun () -> deterministic := true);
+        "-permissive", Unit (fun () -> permissive := true);
       ]
       false
       all_options
@@ -417,6 +427,7 @@ let journal_isset = !journal_isset_ref
 let use_obj = !use_obj_ref
 let use_type = !use_type_ref
 let deterministic = !deterministic
+let permissive = !permissive
 
 (* ************************************************************************* *)
 (** {2 Plugin} *)
@@ -762,11 +773,19 @@ let use_cmdline_files = On_Files.extend
 
 let set_files used_loading l =
   Kernel_log.feedback ~dkey "setting files from command lines.";
-  List.iter
-    (fun s ->
-       if s = "" then error "" "has no name. What do you exactly have in mind?";
-       if s.[0] = '-' then error s "is unknown")
-    l;
+  let l =
+    List.fold_right
+      (fun s acc ->
+         if s = "" then
+           if permissive then (warning "" "has no name"; acc)
+           else error "" "has no name. What do you exactly have in mind?"
+         else if s.[0] = '-' then
+           if permissive then (warning s "is unknown"; acc)
+           else error s "is unknown"
+         else
+           s :: acc
+      ) l []
+  in
   assert
     (Kernel_log.verify
        (not (On_Files.is_empty ()))

src/kernel_services/cmdline_parameters/cmdline.mli

@@ -396,6 +396,13 @@ val deterministic: bool
       are acceptable, as reproducibility is more important.
       @since Aluminium-20160501 *)
 
+val permissive: bool
+  (** Downgrades some command-line errors to warnings, such as
+      unknown option names and invalid values for some options
+      (e.g. inexistent function names).
+
+      @since Frama-C+dev *)
+
 val last_project_created_by_copy: (unit -> string option) ref
 
 val load_all_plugins: (unit -> unit) ref

src/kernel_services/cmdline_parameters/parameter_builder.ml

@@ -1031,7 +1031,7 @@ struct
       if must_exist then
         error s
       else
-      if !Parameter_customize.is_permissive_ref then begin
+      if Cmdline.permissive then begin
         P.L.warning "ignoring non-existing function%s '%s'."
           specific_msg s;
         set

src/kernel_services/cmdline_parameters/parameter_customize.ml

@@ -93,8 +93,6 @@ let is_invisible () =
 let use_category_ref = ref true
 let no_category () = use_category_ref := false
 
-let is_permissive_ref = ref false
-
 let find_kf_by_name: (string -> Cil_types.kernel_function) ref =
   Extlib.mk_fun "Parameter_customize.find_kf_by_name"
 

src/kernel_services/cmdline_parameters/parameter_customize.mli

@@ -143,11 +143,6 @@ val no_category: unit -> unit
     @since Sodium-20150201
  *)
 
-val is_permissive_ref: bool ref
-(** if [true], less checks are performed on value of arguments.
-    Set by {!Kernel.Permissive} option
- *)
-
 (* ************************************************************************* *)
 (** {2 Function names} *)
 (* ************************************************************************* *)

src/kernel_services/plugin_entry_points/kernel.ml

@@ -521,23 +521,6 @@ let () =
   Quiet.add_set_hook
     (fun _ b -> assert b; GeneralVerbose.set 0; GeneralDebug.set 0)
 
-let () = Parameter_customize.set_group messages
-let () = Parameter_customize.set_cmdline_stage Cmdline.Early
-let () = Parameter_customize.do_not_projectify ()
-let () = Parameter_customize.do_not_journalize ()
-module Permissive =
-  Bool
-    (struct
-      let default = !Parameter_customize.is_permissive_ref
-      let option_name = "-permissive"
-      let module_name = "Permissive"
-      let help =
-        "performs less verification on validity of command-line options"
-    end)
-let () =
-  Permissive.add_set_hook
-    (fun _ b -> Parameter_customize.is_permissive_ref := b)
-
 let () = Parameter_customize.set_group messages
 let () = Parameter_customize.set_cmdline_stage Cmdline.Extended
 let () = Parameter_customize.do_not_journalize ()
@@ -1650,11 +1633,45 @@ let () =
        Project.Datatype.Set.iter (fun project -> Project.remove ~project ()) s)
 
 (* ************************************************************************* *)
-(** {2 Others options} *)
+(** {2 Checks} *)
+(* ************************************************************************* *)
+
+let checks = add_group "Checks"
+
+let () = Parameter_customize.set_group checks
+let () = Parameter_customize.do_not_reset_on_copy ()
+module Check =
+  False(struct
+    let option_name = "-check"
+    let module_name = "Check"
+    let help = "performs consistency checks over the Abstract Syntax \
+                Tree"
+  end)
+
+let () = Parameter_customize.set_group checks
+module Copy =
+  False(struct
+    let option_name = "-copy"
+    let module_name = "Copy"
+    let help =
+      "always perform a copy of the original AST before analysis begin"
+  end)
+
+let () = Parameter_customize.set_group checks
+let () = Parameter_customize.set_negative_option_name ""
+module TypeCheck =
+  True(struct
+    let module_name = "TypeCheck"
+    let option_name = "-typecheck"
+    let help = "forces typechecking of the source files"
+  end)
+
+(* ************************************************************************* *)
+(** {2 Other options} *)
 (* ************************************************************************* *)
 
 [@@@warning "-60"]
-(* Warning this three options are parsed and used directly from Cmdline *)
+(* Warning: these options are parsed and used directly from Cmdline *)
 
 let () = Parameter_customize.set_negative_option_name ""
 let () = Parameter_customize.set_cmdline_stage Cmdline.Early
@@ -1692,41 +1709,19 @@ module Deterministic =
       let help = ""
     end)
 
-[@@@warning "+60"]
-
-(* ************************************************************************* *)
-(** {2 Checks} *)
-(* ************************************************************************* *)
-
-let checks = add_group "Checks"
-
-let () = Parameter_customize.set_group checks
-let () = Parameter_customize.do_not_reset_on_copy ()
-module Check =
-  False(struct
-    let option_name = "-check"
-    let module_name = "Check"
-    let help = "performs consistency checks over the Abstract Syntax \
-                Tree"
-  end)
-
-let () = Parameter_customize.set_group checks
-module Copy =
-  False(struct
-    let option_name = "-copy"
-    let module_name = "Copy"
-    let help =
-      "always perform a copy of the original AST before analysis begin"
-  end)
-
 let () = Parameter_customize.set_group checks
 let () = Parameter_customize.set_negative_option_name ""
-module TypeCheck =
-  True(struct
-    let module_name = "TypeCheck"
-    let option_name = "-typecheck"
-    let help = "forces typechecking of the source files"
-  end)
+let () = Parameter_customize.set_cmdline_stage Cmdline.Early
+module Permissive =
+  False
+    (struct
+      let module_name = "Permissive"
+      let option_name = "-permissive"
+      let help =
+        "perform less verifications on validity of command-line options"
+    end)
+
+[@@@warning "+60"]
 
 (*
 Local Variables:

src/kernel_services/plugin_entry_points/kernel.mli

@@ -246,6 +246,9 @@ module GeneralDebug: Parameter_sig.Int
 module Quiet: Parameter_sig.Bool
 (** Behavior of option "-quiet" *)
 
+module Permissive: Parameter_sig.Bool
+(** Behavior of option "-permissive" *)
+
 (** @plugin development guide *)
 module Unicode: sig
   include Parameter_sig.Bool

tests/misc/oracle/permissive.res.oracle

+[kernel] Warning: option `-non-existing-option' is unknown, ignoring. [-permissive]
+[kernel] Parsing tests/misc/permissive.i (no preprocessing)
+[kernel] Warning: ignoring non-existing function 'non_existing_function'.

tests/misc/permissive.i

+/*run.config
+  OPT: -permissive -non-existing-option -inline-calls non_existing_function
+*/
+
+void main() {
+}