diff --git a/Changelog b/Changelog index ca81d8698f74c64ed4d224ea0a0cdaeb0dd06da9..ee5fa2758a27896de38d6a84255a68ef2b95a78c 100644 --- a/Changelog +++ b/Changelog @@ -17,6 +17,7 @@ Open Source Release <next-release> ################################## +-* Slicing [2020-09-07] Better handling of invalid command line options. - Eva [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml index a549613bcff45232e21da27a3c709cae9b1b14da..f4f31d5622ae6f8614aff90945b21ee9aa54ed87 100644 --- a/src/plugins/slicing/slicingCmds.ml +++ b/src/plugins/slicing/slicingCmds.ml @@ -529,6 +529,7 @@ let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~lo (** Registered as a slicing selection function: Add a selection of the annotations related to a function. *) let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var kf = + try let zones_decl_vars,pragmas = !Db.Properties.Interp.To_zone.from_func_annots Kinstr.iter_from_func (Some @@ -538,6 +539,13 @@ let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loo kf in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf + with Kernel_function.No_Definition -> + SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline + "No definition for function '%a'. \ + Slicing requests from the command line are ignored." + Kernel_function.pretty kf; + Cil_datatype.Varinfo.Map.empty + (** Registered as a slicing selection function: Add selection of function outputs.