diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index d50b9194b7004e7d3bfc1521f4119f776e9b2c3e..f8866520dde32d6eff48bc98a57be98370d99495 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -78,13 +78,13 @@ PLUGIN_DISTRIB_BIN:=no
 IS_DISTRIBUTED:=no
 ifneq ($(IS_DISTRIBUTED),yes)
 ifeq ($(EACSL_HAS_OCAML312),yes)
-DEV_FLAGS=-warn-error +a
+EACSL_DEV_FLAGS=-warn-error +a
 else
-DEV_FLAGS=-warn-error A
+EACSL_DEV_FLAGS=-warn-error A
 endif
 endif
-PLUGIN_BFLAGS:=$(DEV_FLAGS)
-PLUGIN_OFLAGS:=$(DEV_FLAGS)
+PLUGIN_BFLAGS:=$(EACSL_DEV_FLAGS)
+PLUGIN_OFLAGS:=$(EACSL_DEV_FLAGS)
 
 #######################
 # Local configuration #
@@ -92,13 +92,13 @@ PLUGIN_OFLAGS:=$(DEV_FLAGS)
 
 PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
 
-VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
+EACSL_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
 
 $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
-	$(ECHO) "let version = \""$(VERSION)"\"" >> $@
+	$(ECHO) "let version = \""$(EACSL_VERSION)"\"" >> $@
 	$(CHMOD_RO) $@
 
 ###########
@@ -180,7 +180,7 @@ e-acsl-distrib: .depend
 	$(RM) -fr $(EXPORT)
 
 WWW	= /localhome/julien/frama-c/doc/www
-install-distrib: e-acsl-distrib
+e-acsl-install-distrib: e-acsl-distrib
 	$(PRINT) Copying to website
 	$(CP) $(EXPORT).tar.gz $(WWW)/distrib/download/e-acsl
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
index ef4250bb9ab0dda88005347c5151f7bd190cf990..5bf750cbbec2c7bd0f762c4848b1fccca4b22ec5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
@@ -1,3 +1,3 @@
-tests/e-acsl-reject/valid_index.i:5:[e-acsl] warning: E-ACSL construct `\valid_index' is not yet supported. Ignoring annotation.
+tests/e-acsl-reject/valid_index.i:5:[e-acsl] warning: E-ACSL construct `\valid' is not yet supported. Ignoring annotation.
 [e-acsl] 0 annotation was ignored, being untypable.
 [e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
index b8208d3c1a5dee58b0db8be8e29a430966f8ecf8..f0201b41da74ebba101865216bb1d901c5e11b2a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
@@ -1,3 +1,3 @@
-tests/e-acsl-reject/valid_range.i:5:[e-acsl] warning: E-ACSL construct `\valid_range' is not yet supported. Ignoring annotation.
+tests/e-acsl-reject/valid_range.i:5:[e-acsl] warning: E-ACSL construct `\valid' is not yet supported. Ignoring annotation.
 [e-acsl] 0 annotation was ignored, being untypable.
 [e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index ecd3d46a560021d87f3b3155602b556111e2742c..1384ff91496a1a49a04abee5734525e20a69e6f5 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -384,8 +384,6 @@ let rec type_predicate_named p = match p.content with
   | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
   | Pat(p, _) -> type_predicate_named p
   | Pvalid _ ->  Error.not_yet "\\valid"
-  | Pvalid_index _ -> Error.not_yet "\\valid_index"
-  | Pvalid_range _ -> Error.not_yet "\\valid_range"
   | Pfresh _ -> Error.not_yet "\\fresh"
   | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
   | Pinitialized _ -> Error.not_yet "\\initialized"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index eb1a7593314a57e3388ea88b07624e80b07bf494..c520bdf5806aea091feb62b0b914706e7836f60f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -477,8 +477,6 @@ let rec named_predicate_to_exp ?name env p =
     assert (not is_string);
     e, env
   | Pvalid _ -> Error.not_yet "\\valid"
-  | Pvalid_index _ -> Error.not_yet "\\valid_index"
-  | Pvalid_range _ -> Error.not_yet "\\valid_range"
   | Pfresh _ -> Error.not_yet "\\fresh"
   | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
   | Pinitialized _ -> Error.not_yet "\\initialized"
@@ -587,6 +585,7 @@ let convert_pre_code_annotation env annot =
     | AInvariant(_, b, _) -> assert b; Error.not_yet "loop invariant"
     | AVariant _ -> Error.not_yet "variant"
     | AAssigns _ -> Error.not_yet "assigns"
+    | AAllocation _ -> Error.not_yet "allocation"
     | APragma _ -> Error.not_yet "pragma"
   in
   Error.handle convert env
@@ -598,6 +597,7 @@ let convert_post_code_annotation env annot =
     | AInvariant _ 
     | AVariant _
     | AAssigns _
+    | AAllocation _
     | APragma _ -> env
   in
   Error.handle convert env