From 23ad1517a404d9c1e919904b34c7405c0595c691 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 12 Jun 2020 14:55:31 +0200
Subject: [PATCH] [Eva] Exported function [use_builtin] raises Not_found on
unknown builtins.
---
src/plugins/value/Eva.mli | 5 +++--
src/plugins/value/value_parameters.ml | 8 ++++++--
2 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index a2f023223cc..4de6198ed1a 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -36,8 +36,9 @@ module Value_parameters: sig
(** Returns the list (name, descr) of currently enabled abstract domains. *)
val enabled_domains: unit -> (string * string) list
- (** [use_builtin kf b] adds a builtin override for function [kf] to
- builtin {!b}. *)
+ (** [use_builtin kf name] instructs the analysis to use the builtin [name]
+ to interpret calls to function [kf].
+ Raises [Not_found] if there is no builtin of name [name]. *)
val use_builtin: Cil_types.kernel_function -> string -> unit
end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index cbbdd4865a7..5d65b1fc3ea 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -941,8 +941,12 @@ module BuiltinsOverrides =
end)
let () = add_precision_dep BuiltinsOverrides.parameter
let () = BuiltinsOverrides.add_aliases ["-val-builtin"]
-let use_builtin key value =
- BuiltinsOverrides.add (key, Some value)
+
+(* Exported in Eva.mli. *)
+let use_builtin key name =
+ if !Db.Value.mem_builtin name
+ then BuiltinsOverrides.add (key, Some name)
+ else raise Not_found
let () = Parameter_customize.set_group precision_tuning
module BuiltinsAuto =
--
GitLab