diff --git a/Makefile b/Makefile
index 8a1d9897659a5a16bf966df630a839a416c2f6d5..ca6738ba30a5cec5ba75a291253c14099d1cf5ac 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 f4e68e27934f1498b7287b9f616e3ef08dc3db96..450578e530956ac9c39728e9a0beb5d9c2f781b5 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 62993f4ad6c265b12d7b7112b0c66e5d23f9cae8..0000000000000000000000000000000000000000
--- 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 90ce19fac0aa3e9d74b1b93322aa1c200e906908..0000000000000000000000000000000000000000
--- 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