From 5d0cc350dd1b37599f42f265a325ef16ea4f0857 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Aug 2023 13:52:24 +0200
Subject: [PATCH] [Eva] Removes unused file cilE.ml and function
[Alarmset.notify].
---
src/kernel_services/abstract_interp/cilE.ml | 46 -----------------
src/kernel_services/abstract_interp/cilE.mli | 54 --------------------
src/plugins/eva/alarmset.ml | 28 ----------
src/plugins/eva/alarmset.mli | 4 --
4 files changed, 132 deletions(-)
delete mode 100644 src/kernel_services/abstract_interp/cilE.ml
delete mode 100644 src/kernel_services/abstract_interp/cilE.mli
diff --git a/src/kernel_services/abstract_interp/cilE.ml b/src/kernel_services/abstract_interp/cilE.ml
deleted file mode 100644
index f650d8e3a6d..00000000000
--- a/src/kernel_services/abstract_interp/cilE.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(* ************************************************************************* *)
-(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
- plug-in. Refactoring required. *)
-(* ************************************************************************* *)
-
-type alarm_behavior = unit -> unit
-
-let a_ignore = Extlib.nop
-
-type warn_mode = {defined_logic: alarm_behavior;
- unspecified: alarm_behavior;
- others: alarm_behavior;}
-
-let warn_none_mode =
- { defined_logic = a_ignore; unspecified = a_ignore; others = a_ignore; }
-
-
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/cilE.mli b/src/kernel_services/abstract_interp/cilE.mli
deleted file mode 100644
index cb0e2d41d37..00000000000
--- a/src/kernel_services/abstract_interp/cilE.mli
+++ /dev/null
@@ -1,54 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Value analysis alarms *)
-
-(* ************************************************************************* *)
-(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
- plug-in. Refactoring required. *)
-(* ************************************************************************* *)
-
-type alarm_behavior = unit -> unit
-
-val a_ignore: alarm_behavior
-
-type warn_mode =
- { defined_logic: alarm_behavior
- (** operations that raise an error only in the C, not in the logic *);
- unspecified: alarm_behavior (** defined but unspecified behaviors *);
- others: alarm_behavior (** all the remaining undefined behaviors *);
- }
-(** An argument of type [warn_mode] can be supplied to some of the access
- functions in {!Db.Value} (the interface to the value analysis).
- Each field of {!warn_mode} indicates the action to perform
- for each category of alarm. These fields are not completely fixed
- yet. However, you can use the value {!warn_none_mode} below
- when you have to provide an argument of type [warn_mode]. *)
-
-val warn_none_mode : warn_mode
-(** Do not emit any message. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/eva/alarmset.ml b/src/plugins/eva/alarmset.ml
index d902c0d852f..88c99208679 100644
--- a/src/plugins/eva/alarmset.ml
+++ b/src/plugins/eva/alarmset.ml
@@ -205,8 +205,6 @@ let for_all test ~default = function
Alarms
------------------------------------------------------------------------ *)
-open CilE
-
let emitter = Eva_utils.emitter
(* Printer that shows additional information about temporaries *)
@@ -432,32 +430,6 @@ let emit kinstr = function
"All alarms may arise: \
abstract state too imprecise to continue the analysis."
-let warn_alarm warn_mode = function
- | Alarms.Uninitialized _
- | Alarms.Dangling _
- -> warn_mode.unspecified ()
- | Alarms.Pointer_comparison _
- | Alarms.Differing_blocks _
- -> warn_mode.defined_logic ()
- | Alarms.Division_by_zero _
- | Alarms.Overflow _
- | Alarms.Float_to_int _
- | Alarms.Invalid_shift _
- | Alarms.Memory_access _
- | Alarms.Index_out_of_bound _
- | Alarms.Invalid_pointer _
- | Alarms.Is_nan_or_infinite _
- | Alarms.Is_nan _
- | Alarms.Not_separated _
- | Alarms.Overlap _
- | Alarms.Function_pointer _
- | Alarms.Invalid_bool _
- -> warn_mode.others ()
-
-let notify warn_mode alarms =
- iter (fun alarm _status -> warn_alarm warn_mode alarm) alarms
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/eva/alarmset.mli b/src/plugins/eva/alarmset.mli
index 7363b281e6f..850f8e6d7b3 100644
--- a/src/plugins/eva/alarmset.mli
+++ b/src/plugins/eva/alarmset.mli
@@ -104,10 +104,6 @@ val fold : (alarm -> status -> 'a -> 'a) -> 'a -> t -> 'a
instruction. *)
val emit: Cil_types.kinstr -> t -> unit
-(** Calls the functions registered in the [warn_mode] according to the
- set of alarms. *)
-val notify: CilE.warn_mode -> t -> unit
-
val pretty : Format.formatter -> t -> unit
val pretty_status : Format.formatter -> status -> unit
--
GitLab