diff --git a/Makefile b/Makefile index d6d044aebe2a88c183a3477078b4574087e5699d..39a52389bc1ae46a2bb3020873eb27f68062444c 100644 --- a/Makefile +++ b/Makefile @@ -827,7 +827,7 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME))) PLUGIN_ENABLE:=$(ENABLE_EVA) PLUGIN_NAME:=Eva PLUGIN_DIR:=src/plugins/value -PLUGIN_EXTRA_DIRS:=engine values domains domains/cvalue domains/apron \ +PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \ domains/gauges domains/equality legacy partitioning utils gui_files \ values/numerors domains/numerors PLUGIN_TESTS_DIRS+=value/traces @@ -910,10 +910,11 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \ partitioning/partitioning_index partitioning/trace_partitioning \ engine/mem_exec engine/iterator engine/initialization \ engine/compute_functions engine/analysis register \ + api/general_requests \ $(APRON_CMO) $(NUMERORS_CMO) PLUGIN_CMI:= values/abstract_value values/abstract_location \ domains/abstract_domain domains/simpler_domains -PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen +PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server # These files are used by the GUI, but do not depend on Lablgtk VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \ diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 7fdecae8316b409d5dc49098688c2cf5cd52f1a9..8a032485fce6ce08f2de54271969660573acd3e6 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1208,6 +1208,8 @@ src/plugins/value/Changelog_non_free: .ignore src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/api/eva_requests.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/api/eva_requests.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml new file mode 100644 index 0000000000000000000000000000000000000000..1b2c3a0c1c1f49b6e281b37818a24c83b546f543 --- /dev/null +++ b/src/plugins/value/api/general_requests.ml @@ -0,0 +1,38 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +open Server + +let chapter = `Plugin "Eva" +let page = Doc.page chapter ~title:"Eva general services" ~filename:"eva.md" + +module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt) + +let callers kf = + let list = !Db.Value.callers kf in + List.concat (List.map (fun (kf, l) -> List.map (fun s -> kf, s) l) list) + +let () = Request.register ~page + ~kind:`GET ~name:"eva.callers" + ~descr:(Markdown.plain "Get the list of call site of a function") + ~input:(module Kernel_ast.Kf) ~output:(module Data.Jlist (CallSite)) + callers diff --git a/src/plugins/value/api/general_requests.mli b/src/plugins/value/api/general_requests.mli new file mode 100644 index 0000000000000000000000000000000000000000..6568b925a92d2cd9bfb6896e3487b64f3736be10 --- /dev/null +++ b/src/plugins/value/api/general_requests.mli @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + +(** General Eva requests registered in the server. *)