diff --git a/Changelog b/Changelog index 4226a43c880bb1792d91fb8f3ec5ce6041b941a7..fed7cb11a379f3583f554ae6ec6ba15a07589089 100644 --- a/Changelog +++ b/Changelog @@ -18,6 +18,7 @@ Open Source Release <next-release> ################################## +- Kernel [2022-09-07] Improve error message for invalid options -D/-I/-U. o! Configure [2022-07-28] Removed autoconf and configure o! Makefile [2022-07-11] Removed Makefile, Frama-C is now built using Dune 3.x o! Pdg [2022-07-01] Removed from Db. Use proper Pdg API instead. diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml index 16882810a482eb983e10567e1d055eafcbc01eb4..0cb082822481c546680f94f7762df918be87a129 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.ml +++ b/src/kernel_services/cmdline_parameters/cmdline.ml @@ -770,6 +770,24 @@ let set_files used_loading l = 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 + (* Option prefixes -I/-D/-U, from the GCC preprocessor, are commonly + used by mistake; the code below detects them and provides a + helpful error message. *) + if String.length s > 1 && + (s.[1] == 'D' || s.[1] == 'I' || s.[1] == 'U') + then + if permissive then + (warning s ("is invalid in Frama-C, \ + use instead: -cpp-extra-args=\"" ^ s ^ + "\"\n(see option -kernel-h for more information)"); + acc) + else + Kernel_log.abort + "option `%s' is invalid in Frama-C, \ + use instead: -cpp-extra-args=\"%s\"@\n\ + see option -kernel-h for more information." + s s + else if permissive then (warning s "is unknown"; acc) else error s "is unknown" else diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index e74a9d56bb29f89c21dfc3fea853c2e61aa60468..f0da071d53ff16ced72de0b46211f776c161683d 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -995,8 +995,9 @@ module CppExtraArgs = let module_name = "CppExtraArgs" let option_name = "-cpp-extra-args" let arg_name = "args" - let help = "additional arguments passed to the preprocessor while \ - preprocessing the C code but not while preprocessing annotations" + let help = "additional arguments passed to the preprocessor \ + (mainly -D and -I) while preprocessing the C code \ + but not while preprocessing annotations" end) let () = Parameter_customize.set_group parsing