Commit eb10aa7b authored by Julien Signoles's avatar Julien Signoles
Browse files

fixes a few comments

parent f3ca3696
......@@ -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
......
......@@ -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:
......
......@@ -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
......
......@@ -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} *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment