diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 78572f83775819071f278b22995fe41e269c545c..0fea8bfb71a79a2f880769b7dcd3505a7b13e49a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
+-* E-ACSL [2020/01/06] Fix typing bug in presence of variable-length
+ arrays that may lead to incorrect generated code.
-* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
############################
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index fd7d0e6b9675f49ab160839a7324520409c7c15f..b59e1c175936734b7b9001c8bfdb6e9feb453618 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -182,42 +182,37 @@ module Memo: sig
val clear: unit -> unit
end = struct
- module H = Hashtbl.Make(struct
- type t = term
- (* The comparison over terms is the physical equality. It cannot be the
- structural one (given by [Cil_datatype.Term.equal]) because the very
- same term can be used in 2 different contexts which lead to different
- casts.
-
- By construction, there are no physically equal terms in the AST
- built by Cil. Consequently the memoisation should be fully
- useless. However the translation of E-ACSL guarded quantification
- generates new terms (see module {!Quantif}) which must be typed. The
- term corresponding to the bound variable [x] is actually used twice:
- once in the guard and once for encoding [x+1] when incrementing it. The
- memoization is only useful here and indeed prevent the generation of
- one extra variable in some cases. *)
- let equal (t1:term) t2 = t1 == t2
- let hash = Cil_datatype.Term.hash
- end)
-
- let tbl = H.create 97
+ (* The comparison over terms is the physical equality. It cannot be the
+ structural one (given by [Cil_datatype.Term.equal]) because the very same
+ term can be used in 2 different contexts which lead to different casts.
+
+ By construction (see prepare_ast.ml), there are no physically equal terms
+ in the E-ACSL's generated AST. Consequently the memoisation should be fully
+ useless. However:
+ - type info of many terms are accessed several times
+ - the translation of E-ACSL guarded quantifications generates
+ new terms (see module {!Quantif}) which must be typed. The term
+ corresponding to the bound variable [x] is actually used twice: once in the
+ guard and once for encoding [x+1] when incrementing it. The memoization is
+ only useful here and indeed prevent the generation of one extra variable in
+ some cases. *)
+ let tbl = Misc.Id_term.Hashtbl.create 97
let get t =
- try H.find tbl t
+ try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
Options.fatal
"[typing] type of term '%a' was never computed."
Printer.pp_term t
let memo f t =
- try H.find tbl t
+ try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
let x = f t in
- H.add tbl t x;
+ Misc.Id_term.Hashtbl.add tbl t x;
x
- let clear () = H.clear tbl
+ let clear () = Misc.Id_term.Hashtbl.clear tbl
end
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 872847c39d4d4eb06ef6aa3ba1350146fadec2d3..97b2bea3cfa4b28dcce74f7ed444ef4c563a4ea1 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -219,6 +219,19 @@ let name_of_binop = function
| MinusA -> "sub"
| MinusPP | MinusPI | IndexPI | PlusPI -> assert false
+module Id_term =
+ Datatype.Make_with_collections
+ (struct
+ include Cil_datatype.Term
+ let name = "E_ACSL.Id_term"
+ let compare (t1:term) t2 =
+ if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+ let equal (t1:term) t2 = t1 == t2
+ let structural_descr = Structural_descr.t_abstract
+ let rehash = Datatype.identity
+ let mem_project = Datatype.never_any_project
+ end)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 82d10e9d096b78c3b34aac33e24d6b86777fdba1..a39917f6cc12fcdf867d031ab4c610a69a452994 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -102,6 +102,9 @@ val name_of_binop: binop -> string
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+module Id_term: Datatype.S_with_collections with type t = term
+(** datatype for terms that relies on physical equality *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index d7988858a84f16b79d0baadc1e562207fc70a3df..d015c335f8d801fc8a70bf8d108e3ff5ecb2eae5 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -69,6 +69,17 @@ class prepare_visitor = object (self)
val mutable has_new_stmt_in_fundec = false
val mutable has_new_stmt = false
+ val terms = Misc.Id_term.Hashtbl.create 7
+
+ method !vterm _t =
+ Cil.DoChildrenPost
+ (fun t ->
+ if Misc.Id_term.Hashtbl.mem terms t then
+ (* remove term sharing for soundness of E-ACSL typing
+ (see typing.ml) *)
+ { t with term_node = t.term_node }
+ else
+ t)
(* Add align attributes to local variables (required by temporal analysis) *)
method !vblock _ =
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index e33346236015bde2cddabc58584205d7a1fafb58..b23a84d6295060acf5d0d6e10fbf0dab760d033a 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -23,6 +23,7 @@
(** Prepare AST for E-ACSL generation.
So for this module performs the following tasks:
+ - remove term sharing
- move declarations of variables declared in the bodies of switch
statements to upper scopes;
- store what is necessary to translate in [Keep_status]
diff --git a/src/plugins/e-acsl/tests/memory/vla.c b/src/plugins/e-acsl/tests/memory/vla.c
index 79b15c3475b06690f3a5d238c82ce2eefd575efa..28b41333424bdc50255fde6f48198b70782ce705 100644
--- a/src/plugins/e-acsl/tests/memory/vla.c
+++ b/src/plugins/e-acsl/tests/memory/vla.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: Check variable-length arrays
+ COMMENT: check variable-length arrays
*/
int LEN = 10;