Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
53842f19
Commit
53842f19
authored
2 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[From] Removes exported functions from Db.
parent
d6c4ede6
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/kernel_services/plugin_entry_points/db.ml
+0
-25
0 additions, 25 deletions
src/kernel_services/plugin_entry_points/db.ml
src/kernel_services/plugin_entry_points/db.mli
+1
-37
1 addition, 37 deletions
src/kernel_services/plugin_entry_points/db.mli
with
1 addition
and
62 deletions
src/kernel_services/plugin_entry_points/db.ml
+
0
−
25
View file @
53842f19
...
@@ -674,38 +674,13 @@ module Value = struct
...
@@ -674,38 +674,13 @@ module Value = struct
end
end
module
From
=
struct
module
From
=
struct
exception
Not_lval
exception
Not_lval
let
access
=
mk_fun
"From.access"
let
find_deps_no_transitivity
=
mk_fun
"From.find_deps_no_transitivity"
let
find_deps_no_transitivity
=
mk_fun
"From.find_deps_no_transitivity"
let
find_deps_no_transitivity_state
=
let
find_deps_no_transitivity_state
=
mk_fun
"From.find_deps_no_transitivity_state"
mk_fun
"From.find_deps_no_transitivity_state"
let
find_deps_term_no_transitivity_state
=
let
find_deps_term_no_transitivity_state
=
mk_fun
"From.find_deps_term_no_transitivity_state"
mk_fun
"From.find_deps_term_no_transitivity_state"
let
compute
=
mk_fun
"From.compute"
let
compute_all
=
mk_fun
"From.compute_all"
let
compute_all_calldeps
=
mk_fun
"From.compute_all_calldeps"
let
is_computed
=
mk_fun
"From.is_computed"
let
pretty
=
mk_fun
"From.pretty"
let
get
=
mk_fun
"From.get"
let
self
=
ref
State
.
dummy
let
display
=
mk_fun
"From.display"
module
Record_From_Callbacks
=
Hook
.
Build
(
struct
type
t
=
(
Kernel_function
.
t
Stack
.
t
)
*
Function_Froms
.
Memory
.
t
Stmt
.
Hashtbl
.
t
*
(
Kernel_function
.
t
*
Function_Froms
.
Memory
.
t
)
list
Stmt
.
Hashtbl
.
t
end
)
module
Callwise
=
struct
let
iter
=
mk_fun
"From.Callwise.iter"
let
find
=
mk_fun
"From.Callwise.find"
end
end
end
(* ************************************************************************* *)
(* ************************************************************************* *)
...
...
This diff is collapsed.
Click to expand it.
src/kernel_services/plugin_entry_points/db.mli
+
1
−
37
View file @
53842f19
...
@@ -513,20 +513,6 @@ module From : sig
...
@@ -513,20 +513,6 @@ module From : sig
*)
*)
exception
Not_lval
exception
Not_lval
val
compute_all
:
(
unit
->
unit
)
ref
val
compute_all_calldeps
:
(
unit
->
unit
)
ref
val
compute
:
(
kernel_function
->
unit
)
ref
val
is_computed
:
(
kernel_function
->
bool
)
ref
(** Check whether the from analysis has been performed for the given
function.
@return true iff the analysis has been performed *)
val
get
:
(
kernel_function
->
Function_Froms
.
t
)
ref
val
access
:
(
Locations
.
Zone
.
t
->
Function_Froms
.
Memory
.
t
->
Locations
.
Zone
.
t
)
ref
val
find_deps_no_transitivity
:
(
stmt
->
exp
->
Locations
.
Zone
.
t
)
ref
val
find_deps_no_transitivity
:
(
stmt
->
exp
->
Locations
.
Zone
.
t
)
ref
val
find_deps_no_transitivity_state
:
val
find_deps_no_transitivity_state
:
...
@@ -536,32 +522,10 @@ module From : sig
...
@@ -536,32 +522,10 @@ module From : sig
val
find_deps_term_no_transitivity_state
:
val
find_deps_term_no_transitivity_state
:
(
Cvalue
.
Model
.
t
->
term
->
Value_types
.
logic_dependencies
)
ref
(
Cvalue
.
Model
.
t
->
term
->
Value_types
.
logic_dependencies
)
ref
val
self
:
State
.
t
ref
(** {3 Pretty printing} *)
val
pretty
:
(
Format
.
formatter
->
kernel_function
->
unit
)
ref
val
display
:
(
Format
.
formatter
->
unit
)
ref
(** {3 Callback} *)
module
Record_From_Callbacks
:
Hook
.
Iter_hook
with
type
param
=
Kernel_function
.
t
Stack
.
t
*
Function_Froms
.
Memory
.
t
Stmt
.
Hashtbl
.
t
*
(
Kernel_function
.
t
*
Function_Froms
.
Memory
.
t
)
list
Stmt
.
Hashtbl
.
t
(** {3 Access to callwise-stored data} *)
module
Callwise
:
sig
val
iter
:
((
kinstr
->
Function_Froms
.
t
->
unit
)
->
unit
)
ref
val
find
:
(
kinstr
->
Function_Froms
.
t
)
ref
end
end
end
[
@@
alert
db_deprecated
[
@@
alert
db_deprecated
"Db.From is deprecated and will be removed in a future version \
"Db.From is deprecated and will be removed in a future version \
of Frama-C. Please use the From module instead."
]
of Frama-C. Please use the From module
or the Eva API
instead."
]
(* ************************************************************************* *)
(* ************************************************************************* *)
(** {2 Properties} *)
(** {2 Properties} *)
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment