Skip to content
Snippets Groups Projects
Commit 00688ab0 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Cosmetic changes in abstract_domain.

parent 3c4a12ee
No related branches found
No related tags found
No related merge requests found
...@@ -288,7 +288,7 @@ type init_kind = ...@@ -288,7 +288,7 @@ type init_kind =
It avoids repeating the analysis of a function in equivalent entry states. It avoids repeating the analysis of a function in equivalent entry states.
It uses an over-approximation of the locations possibly read and written It uses an over-approximation of the locations possibly read and written
by a function, and compare the entry states for these locations. *) by a function, and compare the entry states for these locations. *)
module type Recycle = sig module type Reuse = sig
type t (** Type of states. *) type t (** Type of states. *)
(** [relate kf bases state] returns the set of bases [bases] in relation with (** [relate kf bases state] returns the set of bases [bases] in relation with
...@@ -376,7 +376,7 @@ module type S = sig ...@@ -376,7 +376,7 @@ module type S = sig
val reduce_by_predicate: val reduce_by_predicate:
state logic_environment -> state -> predicate -> bool -> state or_bottom state logic_environment -> state -> predicate -> bool -> state or_bottom
(** {3 Miscellaneous } *) (** {3 Scoping and initialization } *)
(** Scoping: abstract transformers for entering and exiting blocks. (** Scoping: abstract transformers for entering and exiting blocks.
The variables should be added or removed from the abstract state here. The variables should be added or removed from the abstract state here.
...@@ -395,12 +395,6 @@ module type S = sig ...@@ -395,12 +395,6 @@ module type S = sig
The first argument is the englobing function. *) The first argument is the englobing function. *)
val leave_scope: kernel_function -> varinfo list -> t -> t val leave_scope: kernel_function -> varinfo list -> t -> t
val enter_loop: stmt -> state -> state
val incr_loop_counter: stmt -> state -> state
val leave_loop: stmt -> state -> state
(** Initialization *)
(** The initial state with which the analysis start. *) (** The initial state with which the analysis start. *)
val empty: unit -> t val empty: unit -> t
...@@ -417,7 +411,13 @@ module type S = sig ...@@ -417,7 +411,13 @@ module type S = sig
of the cvalue implementation of this function in the generic engine. *) of the cvalue implementation of this function in the generic engine. *)
val initialize_variable_using_type: init_kind -> varinfo -> t -> t val initialize_variable_using_type: init_kind -> varinfo -> t -> t
include Recycle with type t := t (** {3 Miscellaneous } *)
val enter_loop: stmt -> state -> state
val incr_loop_counter: stmt -> state -> state
val leave_loop: stmt -> state -> state
include Reuse with type t := t
(** Category for the messages about the domain. (** Category for the messages about the domain.
Must be created through {!Value_parameters.register_category}. *) Must be created through {!Value_parameters.register_category}. *)
......
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
module type Domain = sig module type Domain = sig
include Datatype.S_with_collections include Datatype.S_with_collections
include Abstract_domain.Recycle with type t := t include Abstract_domain.Reuse with type t := t
end end
......
...@@ -25,7 +25,7 @@ open Eval ...@@ -25,7 +25,7 @@ open Eval
module type Domain = sig module type Domain = sig
include Datatype.S_with_collections include Datatype.S_with_collections
include Abstract_domain.Recycle with type t := t include Abstract_domain.Reuse with type t := t
end end
(** Counter that must be used each time a new call is analyzed, in order (** Counter that must be used each time a new call is analyzed, in order
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment