diff --git a/Changelog b/Changelog
index 281ea948fa27ed178cec5f91c07b9b6f16ed3b78..76ba6294e471c5435d907722474eaf0bcee870ab 100644
--- a/Changelog
+++ b/Changelog
@@ -16,6 +16,9 @@
 ##################################
 Open Source Release <next-release>
 ##################################
+
+-   Kernel    [2020-09-21] Option -permissive now allows non-existent option
+              names.
 -   Logic     [2020-09-11] Introduce check-only annotations for
               requires, ensures, loop invariant and lemmas
 -   Kernel    [2020-09-08] Add option -print-cpp-commands, to print the
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 9cc9722f84356709e69e311656a8198cc0b12e4b..8e6729761d0bdd0b4b7f0b6bcdb4dc2ff2325f2f 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/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 ()))
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 025cb25859989a8d7aaf8889f1ad4ae3d0c8ea16..0d90e2d6dbea1ffdbb3e514e184ece74a2416511 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/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. non-existent function names).
+
+      @since Frama-C+dev *)
+
 val last_project_created_by_copy: (unit -> string option) ref
 
 val load_all_plugins: (unit -> unit) ref
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 5675500ced75e97c56b01bcc5e0cf583f2798f12..fbad1cab3272dcb7bec80b992711f55f945b4461 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/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
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.ml b/src/kernel_services/cmdline_parameters/parameter_customize.ml
index 9781ec098dc28cec951d5b2ddbe749758700f7d3..2a6a18e92cd0c0f1a41585c7caae9707f74b2fb5 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.ml
+++ b/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"
 
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index f919786877fadc98dfb96c4f1e0865df2dc1dd41..d26971988256225f5b5f98a82bfb2a7bba4286ee 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/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} *)
 (* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index c4b3ed0833f4d6aad22daa009a0cd4dcf39769bb..83c199a92dc7d091333810fec20b6fb4ef2e30f9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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,48 @@ 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_projectify ()
+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
+let () = Parameter_customize.do_not_projectify ()
+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.do_not_projectify ()
+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 +1712,20 @@ 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.do_not_projectify ()
 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:
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index fd3da8db17cc7c8674824bfa13295693e14ed8d9..4ee7fc8182aca01623a70965cf3d159a2adec3fb 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/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
diff --git a/tests/misc/oracle/permissive.res.oracle b/tests/misc/oracle/permissive.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0ab1f5d114cf413d47315f6682d95541022204dc
--- /dev/null
+++ b/tests/misc/oracle/permissive.res.oracle
@@ -0,0 +1,3 @@
+[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'.
diff --git a/tests/misc/permissive.i b/tests/misc/permissive.i
new file mode 100644
index 0000000000000000000000000000000000000000..2daf3446926c7d8e85aa48810de47946f7b7c64a
--- /dev/null
+++ b/tests/misc/permissive.i
@@ -0,0 +1,6 @@
+/*run.config
+  OPT: -permissive -non-existing-option -inline-calls non_existing_function
+*/
+
+void main() {
+}