From 2e05a7701a43f891978645223fb83c557cb959f9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 1 Sep 2020 09:19:29 +0200
Subject: [PATCH] [Eva] Fixes correctness and precision dependencies for some
Eva parameters.
---
src/plugins/value/value_parameters.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 70fd2b157c3..353dd6bb25c 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -911,7 +911,7 @@ module BuiltinsOverrides =
Fall back to <f> if <ffc> cannot handle its arguments."
let default = Kernel_function.Map.empty
end)
-let () = add_precision_dep BuiltinsOverrides.parameter
+let () = add_correctness_dep BuiltinsOverrides.parameter
(* Exported in Eva.mli. *)
let use_builtin key name =
@@ -987,7 +987,7 @@ module UsePrototype =
let help = "Use the ACSL specification of the functions instead of \
their definitions"
end)
-let () = add_precision_dep UsePrototype.parameter
+let () = add_correctness_dep UsePrototype.parameter
let () = Parameter_customize.set_group precision_tuning
module SkipLibcSpecs =
@@ -1259,6 +1259,7 @@ module AllocReturnsNull=
let help = "Memory allocation built-ins (malloc, calloc, realloc) are \
modeled as nondeterministically returning a null pointer"
end)
+let () = add_correctness_dep AllocReturnsNull.parameter
let () = Parameter_customize.set_group malloc
module MallocLevel =
@@ -1271,6 +1272,7 @@ module MallocLevel =
besides the initial one, for each callstack (defaults to 0)"
end)
let () = MallocLevel.set_range 0 max_int
+let () = add_precision_dep MallocLevel.parameter
(* -------------------------------------------------------------------------- *)
(* --- Deprecated aliases --- *)
--
GitLab