[e-acsl] comments

src/plugins/e-acsl/doc/Changelog

@@ -15,10 +15,13 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+- E-ACSL	[2012/01/20] Use GMP arithmetics only when required
+	        (i.e. mostly never in practice).
+
 ###################################
 Plugin E-ACSL 0.1 Nitrogen_20111001
 ###################################
 
--  E-ACSL         [2012/01/06] First release for the Hi-Lite FUI9 project.
+- E-ACSL	[2012/01/06] First release for the Hi-Lite FUI9 project.
 
 ###################################

src/plugins/e-acsl/typing.ml

@@ -29,7 +29,7 @@ module BI = My_bigint
 let is_representable n _k _s = BI.ge n BI.min_int64 && BI.le n BI.max_int64
 
 (******************************************************************************)
-(** Type Lattice *)
+(** Type Definitions: Intervals *)
 (******************************************************************************)
 
 type eacsl_typ =

src/plugins/e-acsl/typing.mli

@@ -26,21 +26,37 @@ open Cil_types
 (** {2 Typing} *)
 (******************************************************************************)
 
-val typ_of_term: term -> typ
 val type_named_predicate: predicate named -> unit
+(** Compute the type of each term of the given predicate. *)
+
 val type_term: term -> unit
+(** Compute the type of the given term. *)
+
+val typ_of_term: term -> typ
+(** Get the type of the given term. Must have been previously computed. *)
+
 val unsafe_set_term: term -> typ -> unit
+(** Modify the type of the given term. No verification is done to check that the
+    new type is correct. *)
+
 val clear: unit -> unit
+(** Remove all the previously computed types. *)
 
 (******************************************************************************)
 (** {2 Subtyping} *)
 (******************************************************************************)
 
 val principal_type: term -> term -> typ
+(** Get the principal type of the two given terms, that is the type which may
+    contain both of them. Their types must have been previously computed. *)
 
 val context_sensitive: 
   ?loc:location -> Env.t -> typ -> bool -> term option -> exp -> 
   exp * Env.t
+(** [context_sensitive env ty is_mpz_string t_opt e] converts [e] in [env] in
+    such a way that it becomes usable in a context of type [ty]. [t_opt], if
+    any, is a term denoting by [e]. [is_mpz_string] is [true] iff [e] is a
+    string denoting a MPZ integer. *)
 
 val is_representable: My_bigint.t -> ikind -> string option -> bool
 (** Is the given constant representable?
@@ -53,6 +69,8 @@ val is_representable: My_bigint.t -> ikind -> string option -> bool
 val compute_quantif_guards_ref
     : (predicate named -> logic_var list -> predicate named -> 
        (term * relation * logic_var * relation * term) list) ref
+(** Forward reference. *)
+
 
 (*
 Local Variables: