From 1d86aa12f36ae541340550d633e4cda75f2b73bc Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 17 Mar 2011 14:52:48 +0000
Subject: [PATCH] - [configure] search GMP sources - [Makefile] better
generation of local_config.ml - [Options] new options for customized code
generation (unused yet)
---
src/plugins/e-acsl/Makefile.in | 7 +++++--
src/plugins/e-acsl/configure.ac | 28 +++++++++++++++++++++++++---
src/plugins/e-acsl/local_config.mli | 1 +
src/plugins/e-acsl/main.ml | 6 +++++-
src/plugins/e-acsl/options.ml | 27 +++++++++++++++++++++++++++
src/plugins/e-acsl/options.mli | 4 ++++
6 files changed, 67 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 2cc356021f6..61ced853031 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 9f743b15f35..f17e9b947ce 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 aacfa9bd0ba..d95ac1f9414 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 45809d9fe18..d1c26f9f8dc 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 09b5029c3f9..f6cee292b62 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 1989a30b52e..c7bc7e22448 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"
--
GitLab