diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index bc2d25e3edeec9aa496db2bb54df3355916a4fc0..d5d488ff22b009b0dea86cc055aec6f620158d9c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -63,7 +63,8 @@ SRC_ANALYSES:= \
 	exit_points \
 	lscope \
 	interval \
-	typing
+	typing \
+	bound_variables
 SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
 # code generator
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 7f24e72705c0e02ecd7c80e03048f3fed66aaa35..f6e7a2458dea59fa67cbdf6a689c8ea05d0ac378 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -67,6 +67,8 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA
 share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
new file mode 100644
index 0000000000000000000000000000000000000000..eeb8edc7e90b78d38187ceba14d482937130a8d4
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Module for preprocessing the quantified predicates. Predicates with
+    quantifiers are hard to translate, so we delegate some of the work to a
+    preprocessing phase. At the end of this phase, all the quantified predicates
+    should have an associated preprocessed form [vars * goal] where - [vars] is a
+    list of guarded variables in the right order - [goal] is the predicate under
+    the quantifications The guarded variables in the list [vars] are of type
+    [term * logic_var * term * predicate option], where a tuple [(t1,v,t2,p)]
+    indicates that v is a logic variable with the two guards t1 <= x < t2 and p
+    is an additional optional guard to intersect the first guard with the
+    provided type for the variable v *)
+
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
new file mode 100644
index 0000000000000000000000000000000000000000..73faeaec2c0144846c01a155bd7ba3d31c3652ed
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.mli
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+