From eb10aa7ba1aa094debfa314e00168a2495232bd3 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 20 Aug 2019 15:36:24 +0200
Subject: [PATCH] fixes a few comments
---
src/plugins/e-acsl/functions.mli | 2 +-
src/plugins/e-acsl/interval.mli | 9 ++++++---
src/plugins/e-acsl/temporal.ml | 2 +-
src/plugins/e-acsl/typing.mli | 3 +--
4 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index 4c1c01fefda..c549f3abc4c 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -61,7 +61,7 @@ module RTL: sig
val is_rtl_name: string -> bool
(** @return [true] if the prefix of the given name indicates that it
- belongs to the public API of the E-ACSL Runtime Realary *)
+ belongs to the public API of the E-ACSL Runtime Library *)
val is_generated_literal_string_name: string -> bool
(** Same as [is_generated_name] but indicates that the name represents a local
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index e041ef8e7d3..bd97b364289 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -63,7 +63,8 @@ val interv_of_typ: Cil_types.typ -> Ival.t
(** @return the smallest interval which contains the given C type.
@raise Is_a_real if the given type is a float type.
(* TODO: also return is_real=true if ty=Real.t *)
- @raise Not_a_number if the given type does not represent numbers. *)
+ (* TODO RATIONAL: why not returning [-\infty; +\infty]? *)
+ @raise Not_a_number if the given type does not represent any number. *)
(* ************************************************************************** *)
(** {3 Environment for interval computations} *)
@@ -85,8 +86,10 @@ end
val infer: Cil_types.term -> Ival.t
(** [infer t] infers the smallest possible integer interval which the values
of the term can fit in.
- @raise Is_a_real if the term is a float or a real
- @raise Not_a_number if the term does not represent a number. *)
+ @raise Is_a_real if the term is either a float or a real.
+(* TODO RATIONAL: why raising Is_a_real since Eva is able to infer such *)
+ intervals?
+ @raise Not_a_number if the term does not represent any number. *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index e7bf4e97376..d624f2ebd57 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -284,7 +284,7 @@ end = struct
let rhs = Cil.new_exp ~loc (Lval ret) in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
- Realary functions (i.e., with no source code available) that return
+ Library functions (i.e., with no source code available) that return
values are considered to be functions that allocate memory. They are
considered so because they need to be handled exactly as memory
allocating functions, that is, the referent of the returned pointer is
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 38dba48cbd2..b580ec514ff 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -86,8 +86,7 @@ val join: number_ty -> number_ty -> number_ty
(** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
there is no [Other] in argument, this function computes the join of this
semi-lattice. If one of the argument is {!Other}, the function assumes that
- the other argument is also {!Other}. In this case, the result is [Other].
- TODO: is now extended to support reals *)
+ the other argument is also {!Other}. In this case, the result is [Other]. *)
(******************************************************************************)
(** {2 Typing} *)
--
GitLab