diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli index 5470e3dd73d5b8ca541444b39215d255d0d43eb0..daa77f213739efd79b793f54a430ceda36e90fb7 100644 --- a/src/kernel_services/analysis/logic_deps.mli +++ b/src/kernel_services/analysis/logic_deps.mli @@ -94,6 +94,7 @@ val code_annot_filter: of the term result? *) val to_result_from_pred: predicate -> bool -(** The follow declarations are kept for compatibility and should not be used *) +(** The following declarations are kept for compatibility and should not be + used *) exception NYI of string val not_yet_implemented: string ref diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml deleted file mode 100644 index 6c96f61d9b9a3b34dd459b0776c136894184fb06..0000000000000000000000000000000000000000 --- a/src/kernel_services/analysis/logic_interp.ml +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of Frama-C. *) -(* *) -(* Copyright (C) 2007-2022 *) -(* CEA (Commissariat à l'énergie atomique et aux énergies *) -(* alternatives) *) -(* *) -(* you can redistribute it and/or modify it under the terms of the GNU *) -(* Lesser General Public License as published by the Free Software *) -(* Foundation, version 2.1. *) -(* *) -(* It is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Lesser General Public License for more details. *) -(* *) -(* See the GNU Lesser General Public License version 2.1 *) -(* for more details (enclosed in the file licenses/LGPLv2.1). *) -(* *) -(**************************************************************************) - -exception Error = Logic_parse_string.Error - -module To_zone = -struct - exception NYI = Logic_deps.NYI - let not_yet_implemented = Logic_deps.not_yet_implemented -end diff --git a/src/kernel_services/analysis/logic_interp.mli b/src/kernel_services/analysis/logic_interp.mli deleted file mode 100644 index 4e8a7e6d648fc250f0e197a1388088b9045c17fa..0000000000000000000000000000000000000000 --- a/src/kernel_services/analysis/logic_interp.mli +++ /dev/null @@ -1,34 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of Frama-C. *) -(* *) -(* Copyright (C) 2007-2022 *) -(* CEA (Commissariat à l'énergie atomique et aux énergies *) -(* alternatives) *) -(* *) -(* you can redistribute it and/or modify it under the terms of the GNU *) -(* Lesser General Public License as published by the Free Software *) -(* Foundation, version 2.1. *) -(* *) -(* It is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU Lesser General Public License for more details. *) -(* *) -(* See the GNU Lesser General Public License version 2.1 *) -(* for more details (enclosed in the file licenses/LGPLv2.1). *) -(* *) -(**************************************************************************) - -(* This module exists for compatibility only and will be removed in future - versions *) - -open Cil_types - -module To_zone : sig - exception NYI of string - val not_yet_implemented : string ref -end - -exception [@alert deprecated "Use directly Logic_parse_string.Error istead."] - Error of location * string diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml index f70ea067c137d15facfc1e77db02e657758bd98b..8b8b3944fd7b0f9f909c80b45285f440c5bcc763 100644 --- a/src/plugins/slicing/slicingCmds.ml +++ b/src/plugins/slicing/slicingCmds.ml @@ -474,7 +474,7 @@ let get_or_raise (info_data_opt, info_decl) = match info_data_opt with | None -> (* TODO: maybe we can know how to use [info_decl] ? *) SlicingParameters.not_yet_implemented - "%s" !Logic_interp.To_zone.not_yet_implemented + "%s" !Logic_deps.not_yet_implemented | Some info_data -> info_data, info_decl (** Registered as a slicing selection function: diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml index 2915223eec08c36ed39b517038169b951525e899..9bba77427e608749ec3b569c40433dfe6cba409b 100644 --- a/src/plugins/slicing/slicingTransform.ml +++ b/src/plugins/slicing/slicingTransform.ml @@ -260,7 +260,7 @@ module Visibility (SliceName : sig SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.annotation_visible] \ not implemented -> invisible"; false - | Logic_interp.To_zone.NYI msg -> + | Logic_deps.NYI msg -> SlicingParameters.warning ~current:true ~once:true "Dropping unsupported ACSL annotation"; SlicingParameters.debug ~level:2 diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml index bc433062ccc8929f0be579864f7878a07a6f8cee..cdf9349121c2583c00be620840f9a98bfb1a7006 100644 --- a/src/plugins/sparecode/spare_marks.ml +++ b/src/plugins/sparecode/spare_marks.ml @@ -314,7 +314,7 @@ class annot_visitor ~filter pdg = object (self) to_select <- add_nodes_and_undef_to_select true info to_select with Not_found -> () (* unreachable *) - | Logic_interp.To_zone.NYI _ -> + | Logic_deps.NYI _ -> Sparecode_params.warning ~current:true ~once:true "Dropping annotation"; ()