Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
cbf69133
Commit
cbf69133
authored
Jun 24, 2020
by
David Bühler
Browse files
[Eva] New server request "eva.callers" to get the call sites of a function.
parent
cea2ad71
Changes
4
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
cbf69133
...
...
@@ -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
\
...
...
headers/header_spec.txt
View file @
cbf69133
...
...
@@ -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
...
...
src/plugins/value/api/general_requests.ml
0 → 100644
View file @
cbf69133
(**************************************************************************)
(* *)
(* 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
src/plugins/value/api/general_requests.mli
0 → 100644
View file @
cbf69133
(**************************************************************************)
(* *)
(* 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. *)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment