[e-acsl] update according to kernel changes

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
 

src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle

-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.

src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle

-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.

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"

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