From 34264f5b872af4b032e2c49c437e2c5f8921f281 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 20 Jan 2012 10:20:57 +0000
Subject: [PATCH] [e-acsl] comments
---
src/plugins/e-acsl/doc/Changelog | 5 ++++-
src/plugins/e-acsl/typing.ml | 2 +-
src/plugins/e-acsl/typing.mli | 20 +++++++++++++++++++-
3 files changed, 24 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 51dac6a9776..60cb51183fe 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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.
###################################
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 428c76dd7aa..7e2859479b4 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/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 =
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index d843afe3650..9af55e88bd2 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/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:
--
GitLab