From b27c1291d1aa20bbb7567901ff0a31efd7432227 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Mar 2024 09:29:25 +0100
Subject: [PATCH] [Eva] Minor changes in comments about renamed Assigns.t type.
---
src/plugins/eva/Eva.mli | 15 +++++++++------
src/plugins/eva/domains/cvalue/builtins.mli | 6 ++++--
src/plugins/eva/legacy/logic_inout.mli | 2 +-
src/plugins/eva/types/assigns.ml | 7 +++++++
src/plugins/eva/utils/cvalue_callbacks.mli | 7 ++++---
5 files changed, 25 insertions(+), 12 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 8505cb05904..1a8fe1b2101 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -716,8 +716,10 @@ module Builtins: sig
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
c_assigns: (Assigns.t * Locations.Zone.t) option;
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result and of each zone written to. *)
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and of each zone written to.
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
}
(** The result of a builtin can be given in different forms. *)
@@ -763,9 +765,10 @@ module Cvalue_callbacks: sig
type state = Cvalue.Model.t
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and the dependencies of each zone written to;
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
@@ -858,7 +861,7 @@ module Logic_inout: sig
Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
(** Evaluate the assigns clauses of the given function in its given pre-state,
- and compare them with the given froms (computed by the from plugin).
+ and compare them with the dependencies computed by the from plugin.
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.t -> unit
diff --git a/src/plugins/eva/domains/cvalue/builtins.mli b/src/plugins/eva/domains/cvalue/builtins.mli
index e090c1daa38..bf85aba9659 100644
--- a/src/plugins/eva/domains/cvalue/builtins.mli
+++ b/src/plugins/eva/domains/cvalue/builtins.mli
@@ -45,8 +45,10 @@ type full_result = {
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
c_assigns: (Assigns.t * Locations.Zone.t) option;
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result and of each zone written to. *)
+ (** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and of each zone written to.
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
}
(** The result of a builtin can be given in different forms. *)
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index acc64743f80..f5f7aaf8295 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -63,7 +63,7 @@ val assigns_tlval_to_zones:
Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
(** Evaluate the assigns clauses of the given function in its given pre-state,
- and compare them with the given froms (computed by the from plugin).
+ and compare them with the dependencies computed by the from plugin.
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.t -> unit
diff --git a/src/plugins/eva/types/assigns.ml b/src/plugins/eva/types/assigns.ml
index f1a4fd3e430..cc34f73bdee 100644
--- a/src/plugins/eva/types/assigns.ml
+++ b/src/plugins/eva/types/assigns.ml
@@ -30,6 +30,7 @@ module DepsOrUnassigned = struct
| AssignedFrom of Deps.t
| MaybeAssignedFrom of Deps.t
[@@deriving eq,ord]
+
let name = "Eva.Froms.DepsOrUnassigned"
let pretty fmt = function
@@ -192,19 +193,25 @@ end
module Datatype_Input = struct
include Datatype.Serializable_undefined
+
type t = {
return : Deps.t;
memory : Memory.t
}
[@@deriving eq,ord]
+
let name = "Eva.Froms"
+
let top = {
return = Deps.top;
memory = Memory.top;
}
+
let reprs = [ top ]
+
let hash assigns =
Hashtbl.hash (Memory.hash assigns.memory, Deps.hash assigns.return)
+
let pretty fmt assigns =
Format.fprintf fmt "%a@\n\\result FROM @[%a@]@\n"
Memory.pretty assigns.memory
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index d5ab270851d..203dddeced3 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -30,9 +30,10 @@
type state = Cvalue.Model.t
-(** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
+(** If not None:
+ - the assigns of the function, i.e. the dependencies of the result
+ and the dependencies of each zone written to;
+ - and its sure outputs, i.e. an under-approximation of written zones. *)
type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
--
GitLab