From 5cbc45cfe2fef90a16ec55e72e755b3cd5d631d2 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 2 Apr 2020 12:06:10 +0200
Subject: [PATCH] [eva] Expose `use_builtin` option in eva's interface
---
src/plugins/value/Eva.mli | 4 ++++
src/plugins/value/value_parameters.ml | 2 ++
src/plugins/value/value_parameters.mli | 4 ++++
3 files changed, 10 insertions(+)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 27f069ce7ee..a2f023223cc 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -35,6 +35,10 @@ end
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}. *)
+ val use_builtin: Cil_types.kernel_function -> string -> unit
end
module Eval_terms: sig
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 82e05def8e6..cbbdd4865a7 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -941,6 +941,8 @@ 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)
let () = Parameter_customize.set_group precision_tuning
module BuiltinsAuto =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8375ac554c7..495d7b1fa9a 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -236,6 +236,10 @@ val register_domain: name:string -> descr:string -> unit
(** Returns the list (name, descr) of currently enabled domains. *)
val enabled_domains: unit -> (string * string) list
+(** [use_builtin kf b] adds a builtin override for function `kf` to
+ builtin `b`. *)
+val use_builtin: Cil_types.kernel_function -> string -> unit
+
(*
Local Variables:
compile-command: "make -C ../../.."
--
GitLab