1
##########################################################################
3
# This file is part of Frama-C. #
5
# Copyright (C) 2007-2008 #
6
# CEA (Commissariat � l'�nergie Atomique) #
7
# INRIA (Institut National de Recherche en Informatique et en #
10
# you can redistribute it and/or modify it under the terms of the GNU #
11
# Lesser General Public License as published by the Free Software #
12
# Foundation, version 2.1. #
14
# It is distributed in the hope that it will be useful, #
15
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
16
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
17
# GNU Lesser General Public License for more details. #
19
# See the GNU Lesser General Public License version v2.1 #
20
# for more details (enclosed in the file licenses/LGPLv2.1). #
22
##########################################################################
25
# autoconf input for Objective Caml programs
26
# Copyright (C) 2001 Jean-Christophe Filli�tre
27
# from a first script by Georges Mariano
29
# the script generated by autoconf from this input will set the following
31
# OCAMLC "ocamlc" if present in the path, or a failure
32
# or "ocamlc.opt" if present with same version number as ocamlc
33
# OCAMLOPT "ocamlopt" (or "ocamlopt.opt" if present), or "no"
34
# OCAMLBEST either "byte" if no native compiler was found,
37
# OCAMLLEX "ocamllex" (or "ocamllex.opt" if present)
38
# OCAMLYACC "ocamlyacc"
39
# OCAMLLIB the path to the ocaml standard library
40
# OCAMLVERSION the ocaml version number
41
# OCAMLWIN32 "yes"/"no" depending on Sys.os_type = "Win32"
42
# EXE ".exe" if OCAMLWIN32=yes, "" otherwise
45
export CYGWIN=nobinmode
48
echo "$1" | tr "a-z" "A-Z"
52
echo "$1" | tr "A-Z" "a-z"
56
banner=`echo "* $1 *" | sed -e 's/./*/g'`
57
title=`echo "* $1 *" | tr "a-z" "A-Z"`
58
AC_MSG_NOTICE($banner)
60
AC_MSG_NOTICE($banner)
63
##########################
64
# Check for Make version #
65
##########################
67
new_section "configure make"
69
AC_CHECK_PROG(MAKE,make,make,)
70
MAKE_DISTRIB=`$MAKE -v | sed -n -e 's/\(.*\) Make.*$/\1/p' `
71
MAKE_MAJOR=`$MAKE -v | sed -n -f bin/sed_get_make_major `
72
MAKE_MINOR=`$MAKE -v | sed -n -f bin/sed_get_make_minor `
73
echo $ECHO_N "make version is $MAKE_DISTRIB Make $MAKE_MAJOR.$MAKE_MINOR: $ECHO_C"
74
if test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;
77
AC_MSG_ERROR([unsupported version; GNU Make version 3.81
78
or higher is required.]);
84
AC_ARG_ENABLE(verbosemake,[ --enable-verbosemake verbose makefile commands],VERBOSEMAKE=yes,VERBOSEMAKE=no)
85
if test "$VERBOSEMAKE" = yes ; then
86
AC_MSG_RESULT(Make will be verbose.)
89
#############################
90
# Check for Ocaml compilers #
91
#############################
93
# Specifically allow 3.10.0
95
AC_ARG_ENABLE(unsupported-ocaml,
96
[ --enable-unsupported-ocaml
97
attempt to compile even against unsupported ocaml version],
98
UNSUPPORTED_OCAML=yes,UNSUPPORTED_OCAML=no)
100
new_section "configure ocaml compilers"
102
# we first look for ocamlc in the path; if not present, we fail
103
AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
104
if test "$OCAMLC" = no ; then
105
AC_MSG_ERROR(Cannot find ocamlc.)
108
# we extract Ocaml version number and library path
109
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
111
echo $ECHO_N "ocaml version is $OCAMLVERSION: $ECHO_C"
112
case $OCAMLVERSION in
113
3.09.3*) echo "${ECHO_T}Good!";;
114
3.09*) echo "${ECHO_T}Warning: unsupported version.";
115
if test "$UNSUPPORTED_OCAML" == "yes"; then
116
echo "Compile at your own risks";
118
echo "If you want to compile Frama-C with this version, use the \
119
--enable-unsupported-ocaml option of configure";
123
3.0*) echo "${ECHO_T}Incompatible version!"; exit 2;;
124
3.10.0) echo "${ECHO_T}Warning: unsupported version." ;
125
if test "$UNSUPPORTED_OCAML" == "yes"; then
126
echo "Compile at your own risks";
128
echo "If you want to compile Frama-C with this version, use the \
129
--enable-unsupported-ocaml option of configure";
133
3.10*) echo "${ECHO_T}Good!";;
134
3.1*) LOWER_THAN_311=no;
135
echo "${ECHO_T}Good!";;
136
*) echo "${ECHO_T}Incompatible version!"; exit 2;;
140
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
141
echo "ocaml library path is $OCAMLLIB"
143
# then we look for ocamlopt; if not present, we issue a warning
144
# if the version is not the same, we also discard it
145
# we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not
146
AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no)
148
if test "$OCAMLOPT" = no ; then
149
AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
151
AC_MSG_CHECKING(ocamlopt version)
152
TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
153
if test "$TMPVERSION" != "$OCAMLVERSION" ; then
154
AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
162
if test "$OCAMLBEST" = "opt"; then
170
# checking for ocamlc.opt
171
AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
172
if test "$OCAMLCDOTOPT" != no ; then
173
AC_MSG_CHECKING(ocamlc.opt version)
174
TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
175
if test "$TMPVERSION" != "$OCAMLVERSION" ; then
176
AC_MSG_RESULT(differs from ocamlc; ocamlc.opt discarded.)
183
# checking for ocamlopt.opt
184
if test "$OCAMLOPT" != no ; then
185
AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no)
186
if test "$OCAMLOPTDOTOPT" != no ; then
187
AC_MSG_CHECKING(ocamlc.opt version)
188
TMPVER=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version *\(.*\)$|\1|p' `
189
if test "$TMPVER" != "$OCAMLVERSION" ; then
190
AC_MSG_RESULT(differs from ocamlc; ocamlopt.opt discarded.)
193
OCAMLOPT=$OCAMLOPTDOTOPT
198
##############################################
199
# Check for other mandatory tools/libraries #
200
##############################################
202
new_section "configure mandatory tools and libraries"
205
AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no)
206
if test "$OCAMLDEP" = no ; then
207
AC_MSG_ERROR(Cannot find ocamldep.)
209
AC_CHECK_PROG(OCAMLDEPDOTOPT,ocamldep.opt,ocamldep.opt,no)
210
if test "$OCAMLDEPDOTOPT" != no ; then
211
OCAMLDEP=$OCAMLDEPDOTOPT
216
AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no)
217
if test "$OCAMLLEX" = no ; then
218
AC_MSG_ERROR(Cannot find ocamllex.)
220
AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no)
221
if test "$OCAMLLEXDOTOPT" != no ; then
222
OCAMLLEX=$OCAMLLEXDOTOPT
227
AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
228
if test "$OCAMLYACC" = no ; then
229
AC_MSG_ERROR(Cannot find ocamlyacc.)
233
dnl AC_CHECK_PROG(CAMLP4OOF,camlp4oof,camlp4oof,no)
234
dnl if test "$CAMLP4OOF" == no ; then
235
dnl case $OCAMLVERSION in
236
dnl 3.09*) CAMLP4OOF="$CAMLP4O pa_macro.cmo pr_o.cmo" ;;
237
dnl *) AC_MSG_ERROR([You need to install camlp4.]);;
243
OCAMLGRAPH_LOCAL=ocamlgraph
246
OCAMLGRAPH_TEST=$OCAMLGRAPH_LOCAL
248
AC_CHECK_FILE($OCAMLGRAPH_TEST,OCAMLGRAPH_EXISTS=yes)
250
if test "$OCAMLGRAPH_EXISTS" == "no"; then
251
AC_CHECK_FILE(ocamlgraph.tar.gz,OCAMLGRAPH_EXISTS=yes)
252
if test "$OCAMLGRAPH_EXISTS" == "yes"; then
253
AC_MSG_NOTICE([Unarchiving ocamlgraph.tar.gz])
254
tar zxf ocamlgraph.tar.gz
257
AC_CHECK_FILE(ocamlgraph.tar.gz,OCAMLGRAPH_TAR=yes)
258
if test "$OCAMLGRAPH_TAR" == "yes"; then
259
if test ocamlgraph.tar.gz -nt ocamlgraph; then
261
AC_MSG_NOTICE([Ocamlgraph updated])
262
tar zxf ocamlgraph.tar.gz
267
#NB: until now, it is not really possible to check a particular
268
#version of ocamlgraph if it is installed system-wide. for godi installs, this
269
#is taken into account by godi itself
270
if test "$OCAMLGRAPH_EXISTS" == "no"; then
272
OCAMLGRAPH_TEST=$OCAMLLIB/ocamlgraph
273
OCAMLGRAPH="-I +ocamlgraph"
274
AC_CHECK_FILE($OCAMLGRAPH_TEST,OCAMLGRAPH_EXISTS=yes)
276
if test "$OCAMLGRAPH_EXISTS" == "no"; then
277
OCAMLGRAPH_TEST=$OCAMLLIB
279
AC_CHECK_FILE($OCAMLGRAPH_TEST/graph.$OBJ_SUFFIX,OCAMLGRAPH_EXISTS=yes)
282
if test "$OCAMLGRAPH_EXISTS" == "no"; then
283
AC_MSG_ERROR(Cannot find $OCAMLGRAPH_LOCAL in current directory
284
Please download the latest version from http://ocamlgraph.lri.fr/download
285
Compile it in "ocamlgraph" then rerun ./configure)
288
AC_CHECK_FILE($OCAMLGRAPH_TEST/Makefile,,
289
AC_MSG_NOTICE([Configuring ocamlgraph])
290
[(cd $OCAMLGRAPH_TEST && ./configure > /dev/null)])
291
# AC_CHECK_FILE($OCAMLGRAPH_TEST/graph.cmo,,
292
# AC_MSG_NOTICE([ocamlgraph not compiled: compiling it])
293
# [$MAKE -s -C $OCAMLGRAPH_TEST])
296
#################################################
297
# Check for other non-mandatory tools/libraries #
298
#################################################
300
new_section "configure non-mandatory tools and libraries"
302
AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,no)
303
if test "$OCAMLDOC" = no ; then
304
AC_MSG_RESULT(ocamldoc discarded not present)
307
AC_CHECK_PROG(OCAMLMKTOP,ocamlmktop,ocamlmktop,no)
308
if test "$OCAMLMKTOP" = no ; then
309
AC_MSG_RESULT(Cannot find ocamlmktop: toplevels cannot be built.)
312
AC_CHECK_PROG(OTAGS,otags,otags,)
313
AC_CHECK_PROG(DOT,dot,dot,)
319
new_section "configure platform"
321
AC_MSG_CHECKING(platform)
322
if echo "let _ = Sys.os_type;;" | ocaml | grep -q Win32; then
328
if echo "let _ = Sys.os_type;;" | ocaml | grep -q Cygwin; then
329
AC_MSG_RESULT(Cygwin)
337
# Local machdep feature (to generate new platforms)
338
AC_ARG_ENABLE(localmachdep,[ --enable-localmachdep enable local machdep configuration],LOCAL_MACHDEP=yes,LOCAL_MACHDEP=no)
340
if test "$LOCAL_MACHDEP" = yes ; then
341
AC_CONFIG_HEADER(config.h)
342
AC_CHECK_HEADERS(stdlib.h)
343
AC_CHECK_HEADERS(wchar.h)
346
# Find out the true definitions of some integer types
347
# checkIntegerype(size_t) will echo "int" or "long"
351
for t in "int" "unsigned int" "long" "unsigned long" "short" "unsigned short" "char" "unsigned char" ;do
352
echo "#include <stddef.h>" >$fn
353
echo "#include <wchar.h>" >>$fn
354
# We define a prototype with one type and the function with
355
# another type. This will result in compilation error
356
# unless the types are really identical
357
echo "$t foo($t x);" >>$fn
358
echo "$1 foo($1 x) { return x;}" >>$fn
359
if gcc -c $fn 2>/dev/null ;then
369
AC_MSG_CHECKING([definition of size_t])
370
TYPE_SIZE_T=`checkIntegerType "size_t"`
371
if test "x$TYPE_SIZE_T" = "x" ;then
372
AC_MSG_ERROR([Cannot find definition of size_t])
374
AC_DEFINE_UNQUOTED(TYPE_SIZE_T, "$TYPE_SIZE_T")
375
AC_MSG_RESULT([$TYPE_SIZE_T])
377
AC_MSG_CHECKING([definition of wchar_t])
378
TYPE_WCHAR_T=`checkIntegerType "wchar_t"`
379
if test "x$TYPE_WCHAR_T" = "x" ;then
380
AC_MSG_ERROR([Cannot find definition of wchar_t])
382
AC_DEFINE_UNQUOTED(TYPE_WCHAR_T, "$TYPE_WCHAR_T")
383
AC_MSG_RESULT([$TYPE_WCHAR_T])
385
AC_MSG_CHECKING([definition of ptrdiff_t])
386
TYPE_PTRDIFF_T=`checkIntegerType "ptrdiff_t"`
387
if test "x$TYPE_PTRDIFF_T" = "x" ;then
388
AC_MSG_ERROR([Cannot find definition of ptrdiff_t])
390
AC_DEFINE_UNQUOTED(TYPE_PTRDIFF_T, "$TYPE_PTRDIFF_T")
391
AC_MSG_RESULT([$TYPE_PTRDIFF_T])
393
AC_MSG_CHECKING([for gcc version])
394
AC_CHECK_TYPE(__builtin_va_list,
395
HAVE_BUILTIN_VA_LIST=true,
396
HAVE_BUILTIN_VA_LIST=false)
397
AC_MSG_CHECKING([if __thread is a keyword])
398
AC_COMPILE_IFELSE([int main(int __thread) { return 0; }],
399
THREAD_IS_KEYWORD=false,
400
THREAD_IS_KEYWORD=true)
401
AC_MSG_RESULT($THREAD_IS_KEYWORD)
403
# Does gcc add underscores to identifiers to make assembly labels?
404
# (I think MSVC always does)
405
AC_MSG_CHECKING([if gcc adds underscores to assembly labels.])
406
AC_LINK_IFELSE([int main() { __asm__("jmp _main"); }],
407
UNDERSCORE_NAME=true,
408
UNDERSCORE_NAME=false)
409
AC_MSG_RESULT($UNDERSCORE_NAME)
413
AC_MSG_CHECKING(if performance counters are usable)
414
# Create a C file from src/perfcount.c.in
416
if gcc -DCONFIGURATION_ONLY \
417
-x c cil/ocamlutil/perfcount.c.in -lm -o bin/cycles.exe >/dev/null 2>&1; then
419
if CYCLES_PER_USEC=`bin/cycles.exe 2>&1` ;then
420
AC_MSG_RESULT([ok ($CYCLES_PER_USEC cycles per us)])
423
AC_MSG_RESULT([no ($CYCLES_PER_USEC)])
428
AC_MSG_RESULT([no (cannot compile perfcount.c)])
432
# If we are on Linux and we use performance counters try to get
433
# the processor speed from /proc/cpuinfo
434
if test "$CYCLES_PER_USEC" != "0" ;then
438
AC_MSG_CHECKING(if /proc/cpuinfo has processor speed)
439
cpuinfo=`cat /proc/cpuinfo 2>/dev/null | grep "cpu MHz"`
440
[procspeed=`echo $cpuinfo | sed 's/^.*[^0-9]\([0-9]\+\.[0-9]\+\).*$/\1/g'`]
441
if test "$procspeed"!="" ;then
442
CYCLES_PER_USEC=$procspeed
443
AC_MSG_RESULT([got $CYCLES_PER_USEC cycles per us])
451
# Now set HAS_PERFCOUNT
461
new_section "wished frama-c plugins"
463
# Library declarations
464
######################
466
# REQUIRE_LIBRARY: library *must* be present in order to build plugins
467
# USE_LIBRARY: better for plugins if library is present, but not required
468
# HAS_LIBRARY: is the library available?
507
### Now plugin declarations
511
define([check_plugin],
513
define([PLUGIN_NAME],$1)
514
define([PLUGIN_FILE],$2)
515
define([PLUGIN_MSG],$3)
516
define([PLUGIN_DEFAULT],$4)
517
default=PLUGIN_DEFAULT
518
AC_CHECK_FILE(PLUGIN_FILE,plugin_present=yes,plugin_present=no;default=no)
520
define([PLUGIN_HELP],
521
AC_HELP_STRING([--enable-PLUGIN_NAME],
522
[PLUGIN_MSG (default: PLUGIN_DEFAULT)]))
530
# Test to change for static plugin, dynamic option
532
#define([PLUGIN_HELP_DYN],
533
# AC_HELP_STRING([--enable-PLUGIN_NAME-dynamic],
534
# [PLUGIN_MSG (default: static)])
535
#define([PLUGIN_NAME_DYN],[PLUGIN_NAME]-dynamic)
541
# ENABLE=$default_dyn
543
#eval ENABLE_DYNAMIC_$up=\$ENABLE
544
if test "$plugin_present" == "no" -a "$FORCE" == "yes"; \
546
AC_MSG_ERROR([PLUGIN_NAME is not available])
548
up=`upper PLUGIN_NAME`
549
eval FORCE_$up=\$FORCE
550
PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}" "FORCE_$up
551
eval ENABLE_$up=\$ENABLE
553
echo "PLUGIN_NAME... $ENABLE"
556
# syntactic callgraph
557
#####################
559
check_plugin(syntactic_callgraph, src/syntactic_callgraph,
560
[support for callgraph plugin], yes)
562
if test "$ENABLE_SYNTACTIC_CALLGRAPH" == "yes"; then
563
USE_GNOMECANVAS=${USE_GNOMECANVAS}" syntactic_callgraph"
564
USE_LABLGTK=${USE_LABLGTK}" syntactic_callgraph"
567
# constant propagation
568
######################
570
check_plugin(constant_propagation, src/constant_propagation,
571
[support for constant propagation plugin], yes)
576
check_plugin(cxx,cxx_elsa,[support for cxx plugin],no)
578
if test "$ENABLE_CXX" == "yes"; then
579
REQUIRE_ELSA=${REQUIRE_ELSA}" cxx"
580
REQUIRE_CAMLP4O=${REQUIRE_CAMLP4O}" cxx"
586
check_plugin(from,src/from,[support for from analysis],yes)
591
check_plugin(gui,src/gui,[support for gui],yes)
593
if test "$ENABLE_GUI" == "yes"; then
594
REQUIRE_LABLGTK=${REQUIRE_LABLGTK}" gui"
600
check_plugin(impact,src/impact,[support for impact plugin],yes)
605
check_plugin(inout,src/inout,[support for inout analysis],yes)
610
check_plugin(jessie,src/jessie,[support for jessie plugin],yes)
612
if test "$ENABLE_JESSIE" == "yes"; then
613
REQUIRE_WHYJC=${REQUIRE_WHYJC}" jessie"
614
USE_APRON=${USE_APRON}" jessie"
620
check_plugin(journal_loader,src/journal_loader,[support journal loading],yes)
625
check_plugin(metrics,src/metrics,[support for metrics analysis],yes)
630
check_plugin(miel,src/miel,[support for miel plugin],no)
632
if test "$ENABLE_MIEL" == "yes"; then
633
REQUIRE_LABLGTK=${REQUIRE_LABLGTK}" miel"
634
REQUIRE_LABLGLADECC=${REQUIRE_LABLGLADECC}" miel"
640
check_plugin(occurrence,src/occurrence,[support for occurrence analysis],yes)
645
dnl check_plugin(occurrence_dyn,src/occurrence_dyn,
646
dnl [support for occurrence analysis (full dynamic)],yes)
651
check_plugin(pdg,src/pdg,[support for pdg plugin],yes)
656
check_plugin(postdominators,src/postdominators,
657
[support for postdominators plugin],yes)
662
check_plugin(scope,src/scope,[support for scope plugin],yes)
667
check_plugin(security,src/security,[support for security plugin],yes)
672
check_plugin(semantic_callgraph,src/semantic_callgraph,
673
[support for semantic_callgraph],yes)
678
check_plugin(slicing,src/slicing,[support for slicing plugin],yes)
683
check_plugin(sparecode,src/sparecode,[support for sparecode plugin],yes)
688
check_plugin(users,src/users,[support for users analysis],yes)
693
check_plugin(value,src/value,[support for value analysis],yes)
698
check_plugin(wp,src/wp,[support for wp plugin],yes)
701
# Aorai : ltl_to_acsl
702
#####################
704
check_plugin(ltl_to_acsl,src/ltl_to_acsl,[support for Aorai plugin (ltl to acsl conversion)],yes)
705
#if test "$ENABLE_LTL_TO_ACSL" == "yes"; then
706
# REQUIRE_LTLTOBA=${REQUIRE_LTLTOBA}" ltl_to_acsl"
711
#####################################################
712
# Check for tools/libraries requirements of plugins #
713
#####################################################
715
new_section "configure tools and libraries used by some plugins"
717
# 1st param: uppercase name of the library
718
# 2nd param: file which must exist. This parameter can be a list of files.
719
# In this case, they will be tried in turn until one of them exists. The
720
# name of the file found will be put in the variable SELECTED_$1
721
# 3d param: warning to display if problem
722
define([configure_library],
724
m4_define([VAR],[$1])
725
m4_define([SELECTED_VAR],[SELECTED_$1])
726
m4_define([PROG],[$2])
727
m4_define([require],[$REQUIRE_$1])
728
m4_define([use],[$USE_$1])
729
m4_define([msg],[$3])
730
m4_define([has],[HAS_$1])
731
m4_define([file],[FILE_$1])
732
if test -n "require" -o -n "use"; then
734
m4_foreach(file,[PROG],
735
[if test "$has" != "yes"; then
736
AC_CHECK_FILE(file,has=yes,has=no)
737
if test "$has" == "yes"; then SELECTED_VAR=file
741
if test "$has" == "no"; then
743
if test "require" != ""; then
744
echo "plugins disabled:
747
fp=FORCE_`upper "$p"`
748
if eval test "\$$fp" == "yes"; then
749
AC_MSG_ERROR($p requested but PROG missing.)
751
ep=ENABLE_`upper "$p"`
752
eval $ep="no\ \(see\ warning\ about\ PROG\)"
755
if test "use" != ""; then
756
echo "plugins not fully functional:
759
ep=ENABLE_`upper "$p"`
761
if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
762
eval $ep="partial\ \(see\ warning\ about\ PROG\)"
769
undefine([SELECTED_VAR])
778
# 1st param: uppercase name of the program
779
# 2nd param: program which must exist. See comment on configure_library()
780
# on how to deal with multiple choices for a given program.
781
# 3d param: warning to display if problem
782
define([configure_tool],
786
define([require],[$REQUIRE_$1])
787
define([use],[$USE_$1])
789
define([has],[HAS_$1])
791
if test -n "require" -o -n "use"; then
794
AC_CHECK_PROG(has,$file,yes,no)
795
if test "$has" == "yes"; then SELECTED_VAR=$file break; fi
797
if test "$has" == "no"; then
799
if test "require" != ""; then
800
echo "plugins disabled:
803
fp=FORCE_`upper "$p"`
804
if eval test "\$$fp" == "yes"; then
805
AC_MSG_ERROR([$p requested but PROG missing.])
807
ep=ENABLE_`upper "$p"`
808
eval $ep="no\ \(see\ warning\ about\ PROG\)"
811
if test "use" != ""; then
812
echo "plugins not fully functional:
815
ep=ENABLE_`upper "$p"`
817
if test "`echo $eep | sed -e 's/ .*//' `" != "no"; then
818
eval $ep="partial\ \(see\ warning\ about\ PROG\)"
837
configure_library([ELSA],[cxx_elsa],[
838
sources of cxx_elsa are not present in this directory.
839
Please check them out from the cvs repository.])
844
if test "$has" == "yes"; then
845
USE_CCPARSE="$REQUIRE_ELSA$USE_ELSA"
848
configure_library([CCPARSE],
849
[cxx_elsa/elsa-2006.06.11/elsa/ccparse],
850
[elsa seems to be uncompiled. Please run 'make elsa'.])
854
configure_tool([LABLGLADECC],[lablgladecc2],[lablgladecc2 not found.])
858
configure_tool([CAMLP4O],[camlp4o],[camlp4o not found.])
862
configure_tool([LTLTOBA],[ltl2ba],[ltl2ba not found.])
866
configure_library([LABLGTK],[$OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX],
867
[lablgtk2/lablgtk.$LIB_SUFFIX not found.])
869
HAS_LABLGTK_CUSTOM_MODEL=no
870
AC_ARG_ENABLE(custommodel,
871
[ --enable-custommodel
872
use a custom tree model in GUI. Need to have a recent lablgtk version],
873
HAS_LABLGTK_CUSTOM_MODEL=yes,HAS_LABLGTK_CUSTOM_MODEL=no)
877
REQUIRE_GTKSOURCEVIEW=
880
FORCE_GTKSOURCEVIEW="yes"
882
if test "$FORCE_GTKSOURCEVIEW" == "yes"; then
883
REQUIRE_GTKSOURCEVIEW="$REQUIRE_LABLGTK"
884
USE_GTKSOURCEVIEW="$USE_LABLGTK"
886
if test "$has" == "yes"; then
887
USE_GTKSOURCEVIEW="$REQUIRE_LABLGTK$USE_LABLGTK"
891
configure_library([GTKSOURCEVIEW],
892
[$OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX,$OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX],
893
[lablgtksourceview.$LIB_SUFFIX not found])
895
case $SELECTED_GTKSOURCEVIEW in
896
$OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX)
897
HAS_LEGACY_GTKSOURCEVIEW=yes
903
configure_library([GNOMECANVAS],[$OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX],
904
[lablgnomecanvas.$LIB_SUFFIX not found])
909
define([WHY_DEFAULT],why)
912
[ --with-whydir=<path> directory for Why sources (default: WHY_DEFAULT) ],
913
WHYDISTRIB=$with_whydir,
914
WHYDISTRIB=WHY_DEFAULT
917
configure_library([WHYJC],
918
[$WHYDISTRIB/jc,$OCAMLLIB/jessie/jc.$OBJ_SUFFIX],
921
configure_library([APRON],
922
[/usr/local/lib/apron.a,/usr/lib/apron.a],
925
if test "$HAS_WHYJC" == "yes" -a "$REQUIRE_WHYJC" != ""; then
926
case $SELECTED_WHYJC in
928
JCCMO=$WHYDISTRIB/jc/jc.cmo
929
JCCMX=$WHYDISTRIB/jc/jc.cmx
931
JESSIE_INCLUDES="-I $WHYDISTRIB/src -I $WHYDISTRIB/jc"
932
(cd $WHYDISTRIB && ./configure --prefix=$prefix --datarootdir=$datarootdir \
933
--exec_prefix=$exec_prefix --bindir=$bindir --libdir=$datadir/frama-c \
934
--mandir=$mandir --enable-apron=$HAS_APRON) || ENABLE_JESSIE=no
935
if test "$ENABLE_JESSIE" == "no"; then
936
INFO_JESSIE=" (configuration of Why failed)"
940
JCCMO=$SELECTED_WHYJC/jc.cmo
941
JCCMX=$SELECTED_WHYJC/jc.cmx
943
JESSIE_INCLUDES="-I $SELECTED_WHYJC"
946
AC_MSG_WARN([Unexpected location for why tool: $SELECTED_WHYJC])
954
#######################
955
# Plugin dependencies #
956
#######################
958
new_section "checking for plugin dependencies"
960
# What are the dependencies?
961
############################
962
# Each plugin has to update these lists
964
REQUIRE_FROM="value inout pdg slicing"
966
#USE_GUI="occurrence security slicing value impact"
968
REQUIRE_PDG="slicing security"
970
REQUIRE_SECURITY="impact"
972
USE_SLICING="security miel"
974
REQUIRE_VALUE="constant_propagation from inout occurrence pdg scope security \
975
slicing sparecode users semantic_callgraph miel"
977
### Now compute the dependencies
978
# a bit ugly... Probably optimizable
980
# First, initialize some variables
981
for fp in ${PLUGINS_FORCE_LIST}; do
982
if test "$fp" != "FORCE_GTKSOURCEVIEW"; then
983
plugin=`echo $fp | sed -e "s/FORCE_\(.*\)/\1/" `
984
TODOLIST=$TODOLIST" "$plugin
986
eval REMEMBER_$plugin=
990
# Implementation of an ordering $1 < $2: "" < yes < partial < no
992
first=`echo "$1" | sed -e 's/ .*//' `
993
second=`echo "$2" | sed -e 's/ .*//' `
999
"partial" | "no") echo "true";;
1003
"yes" | "partial") echo "";;
1010
# Check and propagate marks to requires and users.
1012
# $2: mark to propagate to requires
1013
# $3: mark to propagate to users
1014
check_and_propagate () {
1018
for p in $require; do
1022
if test `lt_mark "$mark" "$2" `; then
1024
eval MARK_$up=\"$2\";
1025
TODOLIST=$TODOLIST" "$p
1026
# display a warning or an error if required
1027
short_mark=`echo $2 | sed -e 's/ .*//'`
1029
reason=`echo $2 | sed -e 's/no (\(.*\))/\1/' `
1030
if test "$short_mark" == "no"; then
1032
if eval test "\$$fp" == "yes"; then
1033
AC_MSG_ERROR([$lp requested but $reason.])
1035
AC_MSG_WARN([$lp disable because $reason.])
1038
if test "$short_mark" == "partial"; then
1039
reason=`echo $2 | sed -e 's/partial (\(.*\))/\1/' `
1040
AC_MSG_WARN([$lp only partially enable because $reason.])
1052
if test `lt_mark "$mark" "$3" `; then
1054
eval MARK_$up=\"$3\";
1055
TODOLIST=$TODOLIST" "$p
1056
# display a warning if required
1058
reason=`echo $3 | sed -e 's/partial (\(.*\))/\1/' `
1059
if test "$reason" != "$3"; then
1060
AC_MSG_WARN([$lp only partially enable because $reason.])
1066
# Recursively check the plugin dependencies using the plugin dependency graph
1067
compute_dependency () {
1068
plugin=`echo $TODOLIST | sed -e 's/ .*//' `
1069
TODOLIST=`echo $TODOLIST | sed -e 's/[[^ ]]* *\(.*\)/\1/' `
1071
lplugin=`lower "$plugin"`
1072
uplugin=`upper "$plugin"`
1073
# new mark to consider
1076
# old mark to consider
1078
eval remember="\$$r"
1079
# the exact mark (final result),
1080
# also the old mark if plugin already visited
1084
# echo "plugin $lplugin (mark=$mark, remember=$remember, enable=$enable)"
1085
if test `lt_mark "$remember" "$mark"`; then
1086
# visit the current plugin:
1087
# mark <- max(mark, enable)
1088
case `echo "$mark" | sed -e 's/ .*//' ` in
1090
if test -n "$enable"; then mark="$enable"; else mark="yes"; fi;;
1091
"partial") if test "$enable" == "no"; then mark="no"; fi;;
1094
# update plugin attributes with the new mark
1095
# echo "update attributes with $mark"
1100
# compute and propagate a new mark to requieres and users
1101
case `echo "$enable" | sed -e 's/ .*//' ` in
1102
"") echo "problem?"; exit 3;;
1103
"yes") check_and_propagate $uplugin "yes" "yes";;
1105
check_and_propagate \
1107
"partial ($lplugin partially enable)" \
1110
check_and_propagate \
1112
"no ($lplugin not enable)" \
1113
"partial ($lplugin not enable)";;
1117
# recursively consider the next plugins
1118
if test -n "$TODOLIST"; then
1126
# Compute INFO_* and exported ENABLE_* from previously computed ENABLE_*
1127
for fp in ${PLUGINS_FORCE_LIST}; do
1128
if test "$fp" != "FORCE_GTKSOURCEVIEW"; then
1129
plugin=`echo $fp | sed -e "s/FORCE_\(.*\)/\1/" `
1132
eval ep_v=`echo $v | sed -e 's/ .*//' `
1133
eval ENABLE_$plugin=$ep_v
1134
reason=`echo $v | sed -e 's/[[a-z]]*\( .*\)/\1/' `
1135
if test "$reason" != "$ep_v"; then
1136
eval INFO_$plugin="\$reason"
1141
############################
1142
# Substitutions to perform #
1143
############################
1145
AC_SUBST(VERBOSEMAKE)
1147
AC_SUBST(OCAMLGRAPH)
1148
AC_SUBST(OCAMLGRAPH_LOCAL)
1150
AC_SUBST(OCAMLVERSION)
1151
AC_SUBST(LOWER_THAN_311)
1153
AC_SUBST(OCAMLWIN32)
1157
AC_SUBST(HAVE_STDLIB_H)
1158
AC_SUBST(HAVE_WCHAR_H)
1159
AC_SUBST(HAVE_PTRDIFF_H)
1160
AC_SUBST(HAVE_BUILTIN_VA_LIST)
1161
AC_SUBST(THREAD_IS_KEYWORD)
1162
AC_SUBST(UNDERSCORE_NAME)
1163
AC_SUBST(HAS_PERFCOUNT)
1164
AC_SUBST(CYCLES_PER_USEC)
1165
AC_SUBST(LOCAL_MACHDEP)
1166
AC_SUBST(datarootdir)
1168
AC_SUBST(HAS_LABLGTK)
1169
AC_SUBST(HAS_GTKSOURCEVIEW)
1170
AC_SUBST(HAS_LEGACY_GTKSOURCEVIEW)
1171
AC_SUBST(HAS_GNOMECANVAS)
1172
AC_SUBST(HAS_LABLGTK_CUSTOM_MODEL)
1173
AC_SUBST(LABLGLADECC)
1174
AC_SUBST(HAS_LABLGLADECC)
1175
AC_SUBST(HAS_LTLTOBA)
1178
AC_SUBST(JESSIE_LOCAL)
1179
AC_SUBST(JESSIE_INCLUDES)
1181
AC_SUBST(ENABLE_SYNTACTIC_CALLGRAPH)
1182
AC_SUBST(ENABLE_CONSTANT_PROPAGATION)
1183
AC_SUBST(ENABLE_CXX)
1184
AC_SUBST(ENABLE_FROM)
1185
AC_SUBST(ENABLE_GUI)
1186
AC_SUBST(ENABLE_IMPACT)
1187
AC_SUBST(ENABLE_INOUT)
1188
AC_SUBST(ENABLE_JESSIE)
1189
AC_SUBST(ENABLE_JOURNAL_LOADER)
1190
AC_SUBST(WHYDISTRIB)
1191
AC_SUBST(ENABLE_METRICS)
1192
AC_SUBST(ENABLE_MIEL)
1193
AC_SUBST(ENABLE_OCCURRENCE)
1194
dnl AC_SUBST(ENABLE_OCCURRENCE_DYN)
1195
AC_SUBST(ENABLE_PDG)
1196
AC_SUBST(ENABLE_POSTDOMINATORS)
1197
AC_SUBST(ENABLE_SCOPE)
1198
AC_SUBST(ENABLE_SECURITY)
1199
AC_SUBST(ENABLE_SEMANTIC_CALLGRAPH)
1200
AC_SUBST(ENABLE_SLICING)
1201
AC_SUBST(ENABLE_SPARECODE)
1202
AC_SUBST(ENABLE_USERS)
1203
AC_SUBST(ENABLE_VALUE)
1205
AC_SUBST(ENABLE_LTL_TO_ACSL)
1207
################################################
1208
# Finally create the Makefile from Makefile.in #
1209
################################################
1211
new_section "creating makefile"
1213
AC_OUTPUT(cil/ocamlutil/perfcount.c Makefile)
1214
chmod a-w cil/ocamlutil/perfcount.c
1221
new_section "summary: plugins available"
1223
if test "$LOWER_THAN_311" == yes ; then
1224
AC_MSG_WARN(Dynamic plugins in native mode are disabled.)
1227
AC_MSG_NOTICE([syntactic callgraph : $ENABLE_SYNTACTIC_CALLGRAPH$INFO_SYNTACTIC_CALLGRAPH])
1228
AC_MSG_NOTICE([constant propagation : $ENABLE_CONSTANT_PROPAGATION$INFO_CONSTANT_PROPAGATION])
1229
AC_MSG_NOTICE([cxx : $ENABLE_CXX$INFO_CXX])
1230
AC_MSG_NOTICE([from : $ENABLE_FROM$INFO_FROM])
1231
AC_MSG_NOTICE([gui : $ENABLE_GUI$INFO_GUI])
1232
AC_MSG_NOTICE([impact : $ENABLE_IMPACT$INFO_IMPACT])
1233
AC_MSG_NOTICE([inout : $ENABLE_INOUT$INFO_INOUT])
1234
AC_MSG_NOTICE([jessie : $ENABLE_JESSIE$INFO_JESSIE])
1235
AC_MSG_NOTICE([journal loader : $ENABLE_JOURNAL_LOADER$INFO_JOURNAL_LOADER])
1236
AC_MSG_NOTICE([metrics : $ENABLE_METRICS$INFO_METRICS])
1237
AC_MSG_NOTICE([miel : $ENABLE_MIEL$INFO_MIEL])
1238
AC_MSG_NOTICE([occurrence : $ENABLE_OCCURRENCE$INFO_OCCURRENCE])
1239
dnl AC_MSG_NOTICE([occurrence dynamic : $ENABLE_OCCURRENCE_DYN$INFO_OCCURRENCE_DYN])
1240
AC_MSG_NOTICE([pdg : $ENABLE_PDG$INFO_PDG])
1241
AC_MSG_NOTICE([postdominators : $ENABLE_POSTDOMINATORS$INFO_POSTDOMINATORS])
1242
AC_MSG_NOTICE([scope : $ENABLE_SCOPE$INFO_SCOPE])
1243
AC_MSG_NOTICE([security : $ENABLE_SECURITY$INFO_SECURITY])
1244
AC_MSG_NOTICE([semantic callgraph : $ENABLE_SEMANTIC_CALLGRAPH$INFO_SEMANTIC_CALLGRAPH])
1245
AC_MSG_NOTICE([slicing : $ENABLE_SLICING$INFO_SLICING])
1246
AC_MSG_NOTICE([spare code : $ENABLE_SPARECODE$INFO_SPARECODE])
1247
AC_MSG_NOTICE([users : $ENABLE_USERS$INFO_USERS])
1248
AC_MSG_NOTICE([value : $ENABLE_VALUE$INFO_VALUE])
1249
AC_MSG_NOTICE([wp : $ENABLE_WP$INFO_WP])
1250
AC_MSG_NOTICE([ltl to acsl : $ENABLE_LTL_TO_ACSL$INFO_LTL_TO_ACSL])
added
removed
configure.in
