doc typing.mli

src/plugins/e-acsl/quantif.ml

@@ -196,7 +196,10 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
         let ty2 = Typing.get_integer_ty t2_one in
         Typing.join ty1 ty2
       in
-      let ty = Typing.typ_of_integer_ty ctx_one in
+      let ty =
+        try Typing.typ_of_integer_ty ctx_one
+        with Typing.Not_an_integer -> assert false
+      in
       (* loop counter corresponding to the quantified variable *)
       let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
       let lv_x = var var_x in

src/plugins/e-acsl/typing.mli

@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Type system which computes the smallest C type that fits to contain all the
+(** Type system which computes the smallest C type that may contain all the
     possible values of a given integer term or predicate. Also compute the
     required casts. *)
 
@@ -30,18 +30,28 @@ open Cil_types
 (** {2 Datatypes} *)
 (******************************************************************************)
 
+(** Types infered by the system. *)
 type integer_ty = private
   | Gmp
   | C_type of ikind
-  | Other
+  | Other (** Any non-integral type *)
+
+(** {3 Smart constructors} *)
 
 val gmp: integer_ty
 val c_int: integer_ty
 val ikind: ikind -> integer_ty
 
+(** {3 Useful operations over {!integer_ty} *)
+
+exception Not_an_integer
 val typ_of_integer_ty: integer_ty -> typ
+(** @return the smallest C type corresponding to an {!integer_ty}.
+    @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}. *)
 
 (******************************************************************************)
 (** {2 Typing} *)
@@ -53,28 +63,41 @@ val type_term: force:bool -> ctx:integer_ty -> term -> unit
     -e-acsl-gmp-only is set. *)
 
 val type_named_predicate: ?must_clear:bool -> predicate named -> unit
-(** Compute the type of each term of the given predicate. *)
+(** Compute the type of each term of the given predicate.
+    Set {!must_clear} to false in order to not reset the environment. *)
+
+val clear: unit -> unit
+(** Remove all the previously computed types. *)
+
+(** {3 Getters}
+
+    Below, the functions assume that either {!type_term} or
+    {!type_named_predicate} has been previously computed for the given term or
+    predicate. *)
 
 val get_integer_ty: term -> integer_ty
+(** @return the infered type for the given term. *)
+
 val get_integer_op: term -> integer_ty
+(** @return the infered type for the top operation of the given term.
+    It is meaningless to call this function over a non-arithmetical/logical
+    operator. *)
+
 val get_integer_op_of_predicate: predicate named -> integer_ty
+(** @return the infered type for the top operation of the given predicate. *)
 
 val get_typ: term -> typ
-(** Get the type of the given term.
-    {!type_named_predicate} must already have been called on the englobing
-    predicate. *)
+(** Get the type which the given term must be generated to. *)
 
 val get_op: term -> typ
+(** Get the type which the operation on top of the given term must be generated
+    to. *)
 
 val get_cast: term -> typ option
-(** Get the type which the given term must be converted to after its translation
-    (if any). {!type_named_predicate} must already have been called on the
-    englobing predicate. *)
+(** Get the type which the given term must be converted to (if any). *)
 
 val get_cast_of_predicate: predicate named -> typ option
-
-val clear: unit -> unit
-(** Remove all the previously computed types. *)
+(** Like {!get_cast}, but for predicates. *)
 
 (******************************************************************************)
 (** {2 Internal stuff} *)