diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 2cc356021f60f54f820c2113458e75b30eb584db..61ced853031ebf39a01823ecb1a81f2a634aff70 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -38,10 +38,13 @@ PLUGIN_DISTRIBUTED:=no
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
 PLUGIN_DISTRIB_BIN:=no
 
-$(PLUGIN_DIR)/local_config.ml:
+$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
+	$(PRINT_MAKING) $@
 	$(RM) $@
-	$(ECHO) "let may_compile_with_cc = @MAY_COMPILE_WITH_CC@" > $@
+	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
+	$(ECHO) "let may_compile_with_cc = @MAY_COMPILE_WITH_CC@" >> $@
 	$(ECHO) "let may_use_assert = @MAY_USE_ASSERT@" >> $@
+	$(ECHO) "let gmpsrc_dir = \"@GMPSRC_DIR@\"" >> $@
 	$(CHMOD_RO) $@
 
 PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 9f743b15f35bf7ea351c723cb291a1a04b7b9b0e..f17e9b947ce4c49d4035927303de81f5ef84de53 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -60,7 +60,7 @@ fi
 if test -z $HAVE_STDIO_H; then
   MAY_COMPILE_WITH_CC=false
   MAY_RUN_TESTS=no
-  AC_MSG_WARN([stdio.h missing: cannot use option -e-acsl-hlink.])
+  AC_MSG_WARN([stdio.h missing: cannot use option -e-acsl-link-headers.])
   AC_MSG_WARN([stdio.h missing: non-regression tests unavailable.])
 fi
 
@@ -72,7 +72,7 @@ AC_CHECK_HEADER(assert.h,HAVE_ASSERT_H=yes,)
 if test -z $HAVE_ASSERT_H; then
   MAY_USE_ASSERT=false
   MAY_RUN_TESTS=no
-  AC_MSG_WARN([assert.h missing: will use exit instead of assert.])
+  AC_MSG_WARN([assert.h missing: cannot use E-ACSL option -e-acsl-use-assert.])
   AC_MSG_WARN([assert.h missing: non-regression tests unavailable.])
 fi
 
@@ -84,10 +84,31 @@ AC_CHECK_LIB(gmp,__gmpz_init,HAVE_GMP=yes,) # also set LIBS
 if test -z $HAVE_GMP; then
   MAY_COMPILE_WITH_CC=false
   MAY_RUN_TESTS=no
-  AC_MSG_WARN([GMP library missing: cannot use option -e-acsl-hlink.])
+  AC_MSG_WARN([GMP library missing: cannot use E-ACSL option -e-acsl-link-headers.])
   AC_MSG_WARN([GMP library missing: non-regression tests unavailable.])
 fi
 
+# GMP sources
+#############
+
+GMPSRC_DIR=
+
+AC_ARG_WITH(gmp-src,
+  AC_HELP_STRING(
+    [--with-gmp-src],
+    [directory containing the source of the GMP library]
+    ))
+
+if test $with_gmp_src = "yes" -o $with_gmp_src = "no" -o $with_gmp_src = ""; \
+then
+  AC_MSG_WARN([GMP sources missing: cannot use E-ACSL option -e-acsl-link-gmpsrc. Set the directory containing these sources with --with-gmp-src=<dirname>.])
+else
+  GMPSRC_DIR=$with_gmp_src
+  AC_CHECK_FILE($GMPSRC_DIR/mpz/init.c,
+    AC_MSG_NOTICE([GMP sources got from $GMPSRC_DIR]),
+    AC_MSG_ERROR([Directory $GMPSRC_DIR does not contain GMP sources.]))
+fi
+
 #######################
 # Generating Makefile #
 #######################
@@ -95,5 +116,6 @@ fi
 AC_SUBST(MAY_COMPILE_WITH_CC)
 AC_SUBST(MAY_USE_ASSERT)
 AC_SUBST(MAY_RUN_TESTS)
+AC_SUBST(GMPSRC_DIR)
 
 write_plugin_config(Makefile)
diff --git a/src/plugins/e-acsl/local_config.mli b/src/plugins/e-acsl/local_config.mli
index aacfa9bd0ba23539d1b34dcc2dd7fb2acc3f1823..d95ac1f941440b7601ca9a532a76bc59aa5baa0b 100644
--- a/src/plugins/e-acsl/local_config.mli
+++ b/src/plugins/e-acsl/local_config.mli
@@ -21,6 +21,7 @@
 
 val may_compile_with_cc: bool
 val may_use_assert: bool
+val gmpsrc_dir: string
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 45809d9fe18a067f47e01fe1f5e18ceef46238a3..d1c26f9f8dcac8e9225d8ce3add7483f57f957eb 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -55,7 +55,11 @@ module Resulting_projects =
       let name = "E-ACSL resulting projects"
       let size = 7
       let kind = `Correctness
-      let dependencies = [ Ast.self ]
+      let dependencies =
+	[ Ast.self;
+	  Options.H_link.self;
+	  Options.Gmpsrc_link.self;
+	  Options.Use_assert.self ]
      end)
 
 let generate_code =
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 09b5029c3f9c678c3c9bc76a082d8ebafe61b403..f6cee292b62a6ee705fc005c30941cbf67eb35ea 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -46,6 +46,33 @@ module Project_name =
       let arg_name = "prj"
      end)
 
+module H_link =
+  False
+    (struct
+      let option_name = "-e-acsl-link-headers"
+      let help = "include standard headers in the new project \
+(unset by default)"
+      let kind = `Correctness
+     end)
+
+module Gmpsrc_link =
+  False
+    (struct
+      let option_name = "-e-acsl-link-gmpsrc"
+      let help = "link against GMP source code in the new project \
+(unset by default)"
+      let kind = `Correctness
+     end)
+
+module Use_assert =
+  False
+    (struct
+      let option_name = "-e-acsl-use-assert"
+      let help = "use C macro `assert' instead of `exit' in the new project \
+(by default, use it whenever possible)"
+      let kind = `Correctness
+     end)
+
 (*
 Local Variables:
 compile-command: "make"
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index 1989a30b52ecdc1059ee9dcc2b67cd0a378df5dd..c7bc7e224487886eccd531569d4dca524d95ff00 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -26,6 +26,10 @@ include S (** implementation of Log.S for E-ACSL *)
 module Check: BOOL
 module Project_name: STRING
 
+module H_link: BOOL
+module Gmpsrc_link: BOOL
+module Use_assert: BOOL
+
 (*
 Local Variables:
 compile-command: "make"