From abe7fd4aa2c30bff98a20bd9bf7032e3d3ee8169 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Sep 2020 12:13:34 +0200
Subject: [PATCH] [Slicing] avoid crash due to invalid command line
---
src/plugins/slicing/slicingCmds.ml | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index a549613bcff..f4f31d5622a 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.
--
GitLab