From 125a44e8553f6708b21918d1e8561c2326b65cd5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 12:23:25 +0100
Subject: [PATCH] [Eva] Removes file mark_noresults.
---
Makefile | 2 +-
src/plugins/value/engine/function_calls.ml | 4 +++
src/plugins/value/utils/mark_noresults.ml | 37 ----------------------
src/plugins/value/utils/mark_noresults.mli | 24 --------------
4 files changed, 5 insertions(+), 62 deletions(-)
delete mode 100644 src/plugins/value/utils/mark_noresults.ml
delete mode 100644 src/plugins/value/utils/mark_noresults.mli
diff --git a/Makefile b/Makefile
index 8a1d9897659..ca6738ba30a 100644
--- a/Makefile
+++ b/Makefile
@@ -865,7 +865,7 @@ endif
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
utils/eva_audit utils/eva_perf utils/eva_annotations \
utils/eva_dynamic utils/eva_utils utils/red_statuses \
- utils/active_behaviors utils/mark_noresults \
+ utils/active_behaviors \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
partitioning/per_stmt_slevel \
diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml
index f4e68e27934..450578e5309 100644
--- a/src/plugins/value/engine/function_calls.ml
+++ b/src/plugins/value/engine/function_calls.ml
@@ -26,6 +26,10 @@ open Eval
let save_results f =
Parameters.ResultsAll.get () && not (Parameters.NoResultsFunctions.mem f)
+let () =
+ Db.Value.no_results :=
+ (fun fd -> not (save_results fd) || not (Parameters.Domains.mem "cvalue"))
+
(* Signal that some results are not stored. The gui or some API calls
may fail ungracefully. *)
let partial_results () =
diff --git a/src/plugins/value/utils/mark_noresults.ml b/src/plugins/value/utils/mark_noresults.ml
deleted file mode 100644
index 62993f4ad6c..00000000000
--- a/src/plugins/value/utils/mark_noresults.ml
+++ /dev/null
@@ -1,37 +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). *)
-(* *)
-(**************************************************************************)
-
-let should_memorize_function f =
- Parameters.ResultsAll.get () &&
- not (Cil_datatype.Fundec.Set.mem
- f (Parameters.NoResultsFunctions.get ()))
-
-let () = Db.Value.no_results :=
- (fun fd -> not (should_memorize_function fd)
- || not (Parameters.Domains.mem "cvalue"))
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/value/utils/mark_noresults.mli b/src/plugins/value/utils/mark_noresults.mli
deleted file mode 100644
index 90ce19fac0a..00000000000
--- a/src/plugins/value/utils/mark_noresults.mli
+++ /dev/null
@@ -1,24 +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). *)
-(* *)
-(**************************************************************************)
-
-(** Are the states of the function analysis saved? *)
-val should_memorize_function: Cil_types.fundec -> bool
--
GitLab