From 924365cd9a3797b032e1358a223bba0f54fd5abe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 14 Jan 2022 22:22:40 +0100
Subject: [PATCH] [Scope] Exports via dynamic the function [rm_asserts], used
by Eva.
---
src/plugins/scope/datascope.ml | 15 +++++++++++++--
1 file changed, 13 insertions(+), 2 deletions(-)
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index d4cab9e063d..26d5806673e 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -28,11 +28,13 @@ open Cil_types
let cat_rm_asserts_name = "rm_asserts"
let () = Plugin.default_msg_keys [cat_rm_asserts_name]
+let name = "scope"
+
module R =
Plugin.Register
(struct
- let name = "scope"
- let shortname = "scope"
+ let name = name
+ let shortname = name
let help = "data dependencies higher level functions"
end)
@@ -694,6 +696,15 @@ let () =
("Value.rm_asserts", Datatype.func Datatype.unit Datatype.unit))
Db.Value.rm_asserts rm_asserts
+let rm_asserts =
+ Dynamic.register
+ ~comment:"Remove redundant alarms. Used by the Eva plugin."
+ ~plugin:name
+ "rm_asserts"
+ Datatype.(func unit unit)
+ ~journalize:true
+ rm_asserts
+
(*
Local Variables:
compile-command: "make -C ../../.."
--
GitLab