From 669d20a5a306f79be1272c4e8c321fc9de383ac1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 9 Jun 2016 10:13:05 +0200
Subject: [PATCH] [doc] improve code documentation
---
src/plugins/e-acsl/interval.ml | 4 ++--
src/plugins/e-acsl/typing.mli | 11 +++++++----
2 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index a7d667993b1..6037ecd4764 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -210,14 +210,14 @@ let rec infer t =
| Tat (t, _) -> infer t
| TBinOp (MinusPP, t, _) ->
(match Cil.unrollType (get_cty t) with
- | TArray(_, _, { scache = Computed n }, _) ->
+ | TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
make Integer.zero (Integer.div (Integer.of_int n) Integer.eight)
| TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tblock_length (_, t)
| Toffset(_, t) ->
(match Cil.unrollType (get_cty t) with
- | TArray(_, _, { scache = Computed n }, _) ->
+ | TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
singleton_of_int nb_bytes
| TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 8c97f43dbeb..3d493f793d5 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -50,7 +50,7 @@ open Cil_types
(** {2 Datatypes} *)
(******************************************************************************)
-(** Types infered by the system. *)
+(** Possible types infered by the system. *)
type integer_ty = private
| Gmp
| C_type of ikind
@@ -66,12 +66,15 @@ val ikind: ikind -> integer_ty
exception Not_an_integer
val typ_of_integer_ty: integer_ty -> typ
-(** @return the smallest C type corresponding to an {!integer_ty}.
+(** @return the C type corresponding to an {!integer_ty}. That is [Gmpz.t ()]
+ for [Gmp] and [TInt(ik, [[]])] for [Ctype ik].
@raise Not_an_integer in case of {!Other}. *)
val join: integer_ty -> integer_ty -> integer_ty
-(** {!integer_ty} is almost a join-semi-lattice: assume that if one argument is
- {!Other}, then the second argument is also {!Other}. *)
+(** {!integer_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]. *)
(******************************************************************************)
(** {2 Typing} *)
--
GitLab