Skip to content
Snippets Groups Projects
Commit 9f77bff7 authored by Temesghen Kahsai's avatar Temesghen Kahsai
Browse files

adding math.smt2

parent 0a6648a3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
autom4te.cache/output.0
+ 1037
− 19
View file @ 9f77bff7
@%:@! /bin/sh @%:@! /bin/sh
@%:@ Guess values for system-dependent variables and create Makefiles. @%:@ Guess values for system-dependent variables and create Makefiles.
@%:@ Generated by GNU Autoconf 2.69 for lustrec 1.1-Unversioned directory. @%:@ Generated by GNU Autoconf 2.69 for lustrec 1.3- 55.
@%:@ @%:@
@%:@ Report bugs to <ploc@garoche.net>. @%:@ Report bugs to <ploc@garoche.net>.
@%:@ @%:@
...@@ -579,8 +579,8 @@ MAKEFLAGS= ...@@ -579,8 +579,8 @@ MAKEFLAGS=
# Identity of this package. # Identity of this package.
PACKAGE_NAME='lustrec' PACKAGE_NAME='lustrec'
PACKAGE_TARNAME='lustrec' PACKAGE_TARNAME='lustrec'
PACKAGE_VERSION='1.1-Unversioned directory' PACKAGE_VERSION='1.3- 55'
PACKAGE_STRING='lustrec 1.1-Unversioned directory' PACKAGE_STRING='lustrec 1.3- 55'
PACKAGE_BUGREPORT='ploc@garoche.net' PACKAGE_BUGREPORT='ploc@garoche.net'
PACKAGE_URL='' PACKAGE_URL=''
...@@ -589,10 +589,18 @@ ac_default_prefix=/usr/local ...@@ -589,10 +589,18 @@ ac_default_prefix=/usr/local
ac_subst_vars='LTLIBOBJS ac_subst_vars='LTLIBOBJS
LIB@&t@OBJS LIB@&t@OBJS
abs_datadir abs_datadir
OBJEXT
EXEEXT
ac_ct_CC
CPPFLAGS
LDFLAGS
CFLAGS
CC
OCAMLBUILD OCAMLBUILD
OCAMLC OCAMLC
SRC_PATH
OCAMLGRAPH_PATH OCAMLGRAPH_PATH
SVN_REVISION VERSION_CODENAME
target_alias target_alias
host_alias host_alias
build_alias build_alias
...@@ -638,7 +646,12 @@ with_ocamlgraph_path ...@@ -638,7 +646,12 @@ with_ocamlgraph_path
' '
ac_precious_vars='build_alias ac_precious_vars='build_alias
host_alias host_alias
target_alias' target_alias
CC
CFLAGS
LDFLAGS
LIBS
CPPFLAGS'
# Initialize some variables set by options. # Initialize some variables set by options.
...@@ -1179,7 +1192,7 @@ if test "$ac_init_help" = "long"; then ...@@ -1179,7 +1192,7 @@ if test "$ac_init_help" = "long"; then
# Omit some internal or obsolete options to make the list less imposing. # Omit some internal or obsolete options to make the list less imposing.
# This message is too long to be a string in the A/UX 3.1 sh. # This message is too long to be a string in the A/UX 3.1 sh.
cat <<_ACEOF cat <<_ACEOF
\`configure' configures lustrec 1.1-Unversioned directory to adapt to many kinds of systems. \`configure' configures lustrec 1.3- 55 to adapt to many kinds of systems.
Usage: $0 [OPTION]... [VAR=VALUE]... Usage: $0 [OPTION]... [VAR=VALUE]...
...@@ -1240,7 +1253,7 @@ fi ...@@ -1240,7 +1253,7 @@ fi
if test -n "$ac_init_help"; then if test -n "$ac_init_help"; then
case $ac_init_help in case $ac_init_help in
short | recursive ) echo "Configuration of lustrec 1.1-Unversioned directory:";; short | recursive ) echo "Configuration of lustrec 1.3- 55:";;
esac esac
cat <<\_ACEOF cat <<\_ACEOF
...@@ -1251,6 +1264,18 @@ Optional Packages: ...@@ -1251,6 +1264,18 @@ Optional Packages:
should be in ocamlgraph-path @<:@default=@S|@(ocamlfind should be in ocamlgraph-path @<:@default=@S|@(ocamlfind
query ocamlgraph)@:>@ query ocamlgraph)@:>@
Some influential environment variables:
CC C compiler command
CFLAGS C compiler flags
LDFLAGS linker flags, e.g. -L<lib dir> if you have libraries in a
nonstandard directory <lib dir>
LIBS libraries to pass to the linker, e.g. -l<library>
CPPFLAGS (Objective) C/C++ preprocessor flags, e.g. -I<include dir> if
you have headers in a nonstandard directory <include dir>
Use these variables to override the choices made by `configure' or to help
it to find libraries and programs with nonstandard names/locations.
Report bugs to <ploc@garoche.net>. Report bugs to <ploc@garoche.net>.
_ACEOF _ACEOF
ac_status=$? ac_status=$?
...@@ -1314,7 +1339,7 @@ fi ...@@ -1314,7 +1339,7 @@ fi
test -n "$ac_init_help" && exit $ac_status test -n "$ac_init_help" && exit $ac_status
if $ac_init_version; then if $ac_init_version; then
cat <<\_ACEOF cat <<\_ACEOF
lustrec configure 1.1-Unversioned directory lustrec configure 1.3- 55
generated by GNU Autoconf 2.69 generated by GNU Autoconf 2.69
Copyright (C) 2012 Free Software Foundation, Inc. Copyright (C) 2012 Free Software Foundation, Inc.
...@@ -1327,11 +1352,95 @@ fi ...@@ -1327,11 +1352,95 @@ fi
## ------------------------ ## ## ------------------------ ##
## Autoconf initialization. ## ## Autoconf initialization. ##
## ------------------------ ## ## ------------------------ ##
@%:@ ac_fn_c_try_compile LINENO
@%:@ --------------------------
@%:@ Try to compile conftest.@S|@ac_ext, and return whether this succeeded.
ac_fn_c_try_compile ()
{
as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
rm -f conftest.$ac_objext
if { { ac_try="$ac_compile"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_compile") 2>conftest.err
ac_status=$?
if test -s conftest.err; then
grep -v '^ *+' conftest.err >conftest.er1
cat conftest.er1 >&5
mv -f conftest.er1 conftest.err
fi
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; } && {
test -z "$ac_c_werror_flag" ||
test ! -s conftest.err
} && test -s conftest.$ac_objext; then :
ac_retval=0
else
$as_echo "$as_me: failed program was:" >&5
sed 's/^/| /' conftest.$ac_ext >&5
ac_retval=1
fi
eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
as_fn_set_status $ac_retval
} @%:@ ac_fn_c_try_compile
@%:@ ac_fn_c_try_link LINENO
@%:@ -----------------------
@%:@ Try to link conftest.@S|@ac_ext, and return whether this succeeded.
ac_fn_c_try_link ()
{
as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
rm -f conftest.$ac_objext conftest$ac_exeext
if { { ac_try="$ac_link"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_link") 2>conftest.err
ac_status=$?
if test -s conftest.err; then
grep -v '^ *+' conftest.err >conftest.er1
cat conftest.er1 >&5
mv -f conftest.er1 conftest.err
fi
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; } && {
test -z "$ac_c_werror_flag" ||
test ! -s conftest.err
} && test -s conftest$ac_exeext && {
test "$cross_compiling" = yes ||
test -x conftest$ac_exeext
}; then :
ac_retval=0
else
$as_echo "$as_me: failed program was:" >&5
sed 's/^/| /' conftest.$ac_ext >&5
ac_retval=1
fi
# Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information
# created by the PGI compiler (conftest_ipa8_conftest.oo), as it would
# interfere with the next link command; also delete a directory that is
# left behind by Apple's compiler. We do this before executing the actions.
rm -rf conftest.dSYM conftest_ipa8_conftest.oo
eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
as_fn_set_status $ac_retval
} @%:@ ac_fn_c_try_link
cat >config.log <<_ACEOF cat >config.log <<_ACEOF
This file contains any messages produced by compilers while This file contains any messages produced by compilers while
running configure, to aid debugging if configure makes a mistake. running configure, to aid debugging if configure makes a mistake.
It was created by lustrec $as_me 1.1-Unversioned directory, which was It was created by lustrec $as_me 1.3- 55, which was
generated by GNU Autoconf 2.69. Invocation command line was generated by GNU Autoconf 2.69. Invocation command line was
$ $0 $@ $ $0 $@
...@@ -1679,12 +1788,14 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $ ...@@ -1679,12 +1788,14 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $
ac_compiler_gnu=$ac_cv_c_compiler_gnu ac_compiler_gnu=$ac_cv_c_compiler_gnu
VERSION_CODENAME="Xia/Zhong-Kang-dev"
# Next release will be
#AC_INIT([lustrec], [1.3], [ploc@garoche.net])
#AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang")
#AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
$as_echo "@%:@define SVN_REVISION \"Unversioned directory\"" >>confdefs.h #AC_SUBST(SVN_REVISION)
...@@ -1709,6 +1820,8 @@ fi ...@@ -1709,6 +1820,8 @@ fi
SRC_PATH=/Users/Teme/Documents/GitHub/lustrec
# Extract the first word of "ocamlc", so it can be a program name with args. # Extract the first word of "ocamlc", so it can be a program name with args.
set dummy ocamlc; ac_word=$2 set dummy ocamlc; ac_word=$2
...@@ -1756,8 +1869,8 @@ $as_echo_n "checking OCaml version... " >&6; } ...@@ -1756,8 +1869,8 @@ $as_echo_n "checking OCaml version... " >&6; }
ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev` ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev`
major=`echo $ocamlc_version | cut -d . -f 1` major=`echo $ocamlc_version | cut -d . -f 1`
minor=`echo $ocamlc_version | cut -d . -f 2` minor=`echo $ocamlc_version | cut -d . -f 2`
if (test "$major" -lt 3 -a "$minor" -lt 11 ); then if (test "$major" -lt 4 -a "$minor" -lt 0 ); then
as_fn_error $? "Ocaml version must be at least 3.11. You have version $ocamlc_version" "$LINENO" 5 as_fn_error $? "Ocaml version must be at least 4.0. You have version $ocamlc_version" "$LINENO" 5
fi fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: valid ocaml version detected: $ocamlc_version" >&5 { $as_echo "$as_me:${as_lineno-$LINENO}: result: valid ocaml version detected: $ocamlc_version" >&5
$as_echo "valid ocaml version detected: $ocamlc_version" >&6; } $as_echo "valid ocaml version detected: $ocamlc_version" >&6; }
...@@ -1812,13 +1925,893 @@ fi ...@@ -1812,13 +1925,893 @@ fi
$as_echo_n "checking ocamlgraph library... " >&6; } $as_echo_n "checking ocamlgraph library... " >&6; }
ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 -o "graph.cmxa"` ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 -o "graph.cmxa"`
if (test "x$ocamlgraph_lib" = xgraph.cmxa ); then if (test "x$ocamlgraph_lib" = xgraph.cmxa ); then
ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 "graph.cmxa"` ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 "graph.cmxa"`
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: library detected: $ocamlgraph_lib_full " >&5 { $as_echo "$as_me:${as_lineno-$LINENO}: result: library detected: $ocamlgraph_lib_full " >&5
$as_echo "library detected: $ocamlgraph_lib_full " >&6; } $as_echo "library detected: $ocamlgraph_lib_full " >&6; }
else else
as_fn_error $? "ocamlgraph library not installed in $OCAMLGRAPH_PATH" "$LINENO" 5 as_fn_error $? "ocamlgraph library not installed in $OCAMLGRAPH_PATH" "$LINENO" 5
fi fi
ac_ext=c
ac_cpp='$CPP $CPPFLAGS'
ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
ac_compiler_gnu=$ac_cv_c_compiler_gnu
if test -n "$ac_tool_prefix"; then
# Extract the first word of "${ac_tool_prefix}gcc", so it can be a program name with args.
set dummy ${ac_tool_prefix}gcc; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$CC"; then
ac_cv_prog_CC="$CC" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_CC="${ac_tool_prefix}gcc"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
CC=$ac_cv_prog_CC
if test -n "$CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
$as_echo "$CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
fi
if test -z "$ac_cv_prog_CC"; then
ac_ct_CC=$CC
# Extract the first word of "gcc", so it can be a program name with args.
set dummy gcc; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_ac_ct_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$ac_ct_CC"; then
ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_ac_ct_CC="gcc"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
ac_ct_CC=$ac_cv_prog_ac_ct_CC
if test -n "$ac_ct_CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
$as_echo "$ac_ct_CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
if test "x$ac_ct_CC" = x; then
CC=""
else
case $cross_compiling:$ac_tool_warned in
yes:)
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
ac_tool_warned=yes ;;
esac
CC=$ac_ct_CC
fi
else
CC="$ac_cv_prog_CC"
fi
if test -z "$CC"; then
if test -n "$ac_tool_prefix"; then
# Extract the first word of "${ac_tool_prefix}cc", so it can be a program name with args.
set dummy ${ac_tool_prefix}cc; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$CC"; then
ac_cv_prog_CC="$CC" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_CC="${ac_tool_prefix}cc"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
CC=$ac_cv_prog_CC
if test -n "$CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
$as_echo "$CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
fi
fi
if test -z "$CC"; then
# Extract the first word of "cc", so it can be a program name with args.
set dummy cc; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$CC"; then
ac_cv_prog_CC="$CC" # Let the user override the test.
else
ac_prog_rejected=no
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then
ac_prog_rejected=yes
continue
fi
ac_cv_prog_CC="cc"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
if test $ac_prog_rejected = yes; then
# We found a bogon in the path, so make sure we never use it.
set dummy $ac_cv_prog_CC
shift
if test $@%:@ != 0; then
# We chose a different compiler from the bogus one.
# However, it has the same basename, so the bogon will be chosen
# first if we set CC to just the basename; use the full file name.
shift
ac_cv_prog_CC="$as_dir/$ac_word${1+' '}$@"
fi
fi
fi
fi
CC=$ac_cv_prog_CC
if test -n "$CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
$as_echo "$CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
fi
if test -z "$CC"; then
if test -n "$ac_tool_prefix"; then
for ac_prog in cl.exe
do
# Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args.
set dummy $ac_tool_prefix$ac_prog; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$CC"; then
ac_cv_prog_CC="$CC" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_CC="$ac_tool_prefix$ac_prog"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
CC=$ac_cv_prog_CC
if test -n "$CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5
$as_echo "$CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
test -n "$CC" && break
done
fi
if test -z "$CC"; then
ac_ct_CC=$CC
for ac_prog in cl.exe
do
# Extract the first word of "$ac_prog", so it can be a program name with args.
set dummy $ac_prog; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
if ${ac_cv_prog_ac_ct_CC+:} false; then :
$as_echo_n "(cached) " >&6
else
if test -n "$ac_ct_CC"; then
ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test.
else
as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
for as_dir in $PATH
do
IFS=$as_save_IFS
test -z "$as_dir" && as_dir=.
for ac_exec_ext in '' $ac_executable_extensions; do
if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
ac_cv_prog_ac_ct_CC="$ac_prog"
$as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
break 2
fi
done
done
IFS=$as_save_IFS
fi
fi
ac_ct_CC=$ac_cv_prog_ac_ct_CC
if test -n "$ac_ct_CC"; then
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5
$as_echo "$ac_ct_CC" >&6; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi
test -n "$ac_ct_CC" && break
done
if test "x$ac_ct_CC" = x; then
CC=""
else
case $cross_compiling:$ac_tool_warned in
yes:)
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5
$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;}
ac_tool_warned=yes ;;
esac
CC=$ac_ct_CC
fi
fi
fi
test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "no acceptable C compiler found in \$PATH
See \`config.log' for more details" "$LINENO" 5; }
# Provide some information about the compiler.
$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5
set X $ac_compile
ac_compiler=$2
for ac_option in --version -v -V -qversion; do
{ { ac_try="$ac_compiler $ac_option >&5"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_compiler $ac_option >&5") 2>conftest.err
ac_status=$?
if test -s conftest.err; then
sed '10a\
... rest of stderr output deleted ...
10q' conftest.err >conftest.er1
cat conftest.er1 >&5
fi
rm -f conftest.er1 conftest.err
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }
done
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
;
return 0;
}
_ACEOF
ac_clean_files_save=$ac_clean_files
ac_clean_files="$ac_clean_files a.out a.out.dSYM a.exe b.out"
# Try to create an executable without -o first, disregard a.out.
# It will help us diagnose broken compilers, and finding out an intuition
# of exeext.
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C compiler works" >&5
$as_echo_n "checking whether the C compiler works... " >&6; }
ac_link_default=`$as_echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'`
# The possible output files:
ac_files="a.out conftest.exe conftest a.exe a_out.exe b.out conftest.*"
ac_rmfiles=
for ac_file in $ac_files
do
case $ac_file in
*.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;;
* ) ac_rmfiles="$ac_rmfiles $ac_file";;
esac
done
rm -f $ac_rmfiles
if { { ac_try="$ac_link_default"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_link_default") 2>&5
ac_status=$?
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }; then :
# Autoconf-2.13 could set the ac_cv_exeext variable to `no'.
# So ignore a value of `no', otherwise this would lead to `EXEEXT = no'
# in a Makefile. We should not override ac_cv_exeext if it was cached,
# so that the user can short-circuit this test for compilers unknown to
# Autoconf.
for ac_file in $ac_files ''
do
test -f "$ac_file" || continue
case $ac_file in
*.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj )
;;
[ab].out )
# We found the default executable, but exeext='' is most
# certainly right.
break;;
*.* )
if test "${ac_cv_exeext+set}" = set && test "$ac_cv_exeext" != no;
then :; else
ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'`
fi
# We set ac_cv_exeext here because the later test for it is not
# safe: cross compilers may not add the suffix if given an `-o'
# argument, so we may need to know it at that point already.
# Even if this section looks crufty: it has the advantage of
# actually working.
break;;
* )
break;;
esac
done
test "$ac_cv_exeext" = no && ac_cv_exeext=
else
ac_file=''
fi
if test -z "$ac_file"; then :
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
$as_echo "$as_me: failed program was:" >&5
sed 's/^/| /' conftest.$ac_ext >&5
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error 77 "C compiler cannot create executables
See \`config.log' for more details" "$LINENO" 5; }
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
$as_echo "yes" >&6; }
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler default output file name" >&5
$as_echo_n "checking for C compiler default output file name... " >&6; }
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_file" >&5
$as_echo "$ac_file" >&6; }
ac_exeext=$ac_cv_exeext
rm -f -r a.out a.out.dSYM a.exe conftest$ac_cv_exeext b.out
ac_clean_files=$ac_clean_files_save
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of executables" >&5
$as_echo_n "checking for suffix of executables... " >&6; }
if { { ac_try="$ac_link"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_link") 2>&5
ac_status=$?
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }; then :
# If both `conftest.exe' and `conftest' are `present' (well, observable)
# catch `conftest.exe'. For instance with Cygwin, `ls conftest' will
# work properly (i.e., refer to `conftest.exe'), while it won't with
# `rm'.
for ac_file in conftest.exe conftest conftest.*; do
test -f "$ac_file" || continue
case $ac_file in
*.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM | *.o | *.obj ) ;;
*.* ) ac_cv_exeext=`expr "$ac_file" : '[^.]*\(\..*\)'`
break;;
* ) break;;
esac
done
else
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "cannot compute suffix of executables: cannot compile and link
See \`config.log' for more details" "$LINENO" 5; }
fi
rm -f conftest conftest$ac_cv_exeext
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_exeext" >&5
$as_echo "$ac_cv_exeext" >&6; }
rm -f conftest.$ac_ext
EXEEXT=$ac_cv_exeext
ac_exeext=$EXEEXT
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
@%:@include <stdio.h>
int
main ()
{
FILE *f = fopen ("conftest.out", "w");
return ferror (f) || fclose (f) != 0;
;
return 0;
}
_ACEOF
ac_clean_files="$ac_clean_files conftest.out"
# Check that the compiler produces executables we can run. If not, either
# the compiler is broken, or we cross compile.
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are cross compiling" >&5
$as_echo_n "checking whether we are cross compiling... " >&6; }
if test "$cross_compiling" != yes; then
{ { ac_try="$ac_link"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_link") 2>&5
ac_status=$?
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }
if { ac_try='./conftest$ac_cv_exeext'
{ { case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_try") 2>&5
ac_status=$?
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }; }; then
cross_compiling=no
else
if test "$cross_compiling" = maybe; then
cross_compiling=yes
else
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "cannot run C compiled programs.
If you meant to cross compile, use \`--host'.
See \`config.log' for more details" "$LINENO" 5; }
fi
fi
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $cross_compiling" >&5
$as_echo "$cross_compiling" >&6; }
rm -f conftest.$ac_ext conftest$ac_cv_exeext conftest.out
ac_clean_files=$ac_clean_files_save
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of object files" >&5
$as_echo_n "checking for suffix of object files... " >&6; }
if ${ac_cv_objext+:} false; then :
$as_echo_n "(cached) " >&6
else
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
;
return 0;
}
_ACEOF
rm -f conftest.o conftest.obj
if { { ac_try="$ac_compile"
case "(($ac_try" in
*\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
*) ac_try_echo=$ac_try;;
esac
eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\""
$as_echo "$ac_try_echo"; } >&5
(eval "$ac_compile") 2>&5
ac_status=$?
$as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
test $ac_status = 0; }; then :
for ac_file in conftest.o conftest.obj conftest.*; do
test -f "$ac_file" || continue;
case $ac_file in
*.$ac_ext | *.xcoff | *.tds | *.d | *.pdb | *.xSYM | *.bb | *.bbg | *.map | *.inf | *.dSYM ) ;;
*) ac_cv_objext=`expr "$ac_file" : '.*\.\(.*\)'`
break;;
esac
done
else
$as_echo "$as_me: failed program was:" >&5
sed 's/^/| /' conftest.$ac_ext >&5
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "cannot compute suffix of object files: cannot compile
See \`config.log' for more details" "$LINENO" 5; }
fi
rm -f conftest.$ac_cv_objext conftest.$ac_ext
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_objext" >&5
$as_echo "$ac_cv_objext" >&6; }
OBJEXT=$ac_cv_objext
ac_objext=$OBJEXT
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5
$as_echo_n "checking whether we are using the GNU C compiler... " >&6; }
if ${ac_cv_c_compiler_gnu+:} false; then :
$as_echo_n "(cached) " >&6
else
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
#ifndef __GNUC__
choke me
#endif
;
return 0;
}
_ACEOF
if ac_fn_c_try_compile "$LINENO"; then :
ac_compiler_gnu=yes
else
ac_compiler_gnu=no
fi
rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
ac_cv_c_compiler_gnu=$ac_compiler_gnu
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5
$as_echo "$ac_cv_c_compiler_gnu" >&6; }
if test $ac_compiler_gnu = yes; then
GCC=yes
else
GCC=
fi
ac_test_CFLAGS=${CFLAGS+set}
ac_save_CFLAGS=$CFLAGS
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5
$as_echo_n "checking whether $CC accepts -g... " >&6; }
if ${ac_cv_prog_cc_g+:} false; then :
$as_echo_n "(cached) " >&6
else
ac_save_c_werror_flag=$ac_c_werror_flag
ac_c_werror_flag=yes
ac_cv_prog_cc_g=no
CFLAGS="-g"
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
;
return 0;
}
_ACEOF
if ac_fn_c_try_compile "$LINENO"; then :
ac_cv_prog_cc_g=yes
else
CFLAGS=""
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
;
return 0;
}
_ACEOF
if ac_fn_c_try_compile "$LINENO"; then :
else
ac_c_werror_flag=$ac_save_c_werror_flag
CFLAGS="-g"
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
int
main ()
{
;
return 0;
}
_ACEOF
if ac_fn_c_try_compile "$LINENO"; then :
ac_cv_prog_cc_g=yes
fi
rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
fi
rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
fi
rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
ac_c_werror_flag=$ac_save_c_werror_flag
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5
$as_echo "$ac_cv_prog_cc_g" >&6; }
if test "$ac_test_CFLAGS" = set; then
CFLAGS=$ac_save_CFLAGS
elif test $ac_cv_prog_cc_g = yes; then
if test "$GCC" = yes; then
CFLAGS="-g -O2"
else
CFLAGS="-g"
fi
else
if test "$GCC" = yes; then
CFLAGS="-O2"
else
CFLAGS=
fi
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5
$as_echo_n "checking for $CC option to accept ISO C89... " >&6; }
if ${ac_cv_prog_cc_c89+:} false; then :
$as_echo_n "(cached) " >&6
else
ac_cv_prog_cc_c89=no
ac_save_CC=$CC
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
#include <stdarg.h>
#include <stdio.h>
struct stat;
/* Most of the following tests are stolen from RCS 5.7's src/conf.sh. */
struct buf { int x; };
FILE * (*rcsopen) (struct buf *, struct stat *, int);
static char *e (p, i)
char **p;
int i;
{
return p[i];
}
static char *f (char * (*g) (char **, int), char **p, ...)
{
char *s;
va_list v;
va_start (v,p);
s = g (p, va_arg (v,int));
va_end (v);
return s;
}
/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default. It has
function prototypes and stuff, but not '\xHH' hex character constants.
These don't provoke an error unfortunately, instead are silently treated
as 'x'. The following induces an error, until -std is added to get
proper ANSI mode. Curiously '\x00'!='x' always comes out true, for an
array size at least. It's necessary to write '\x00'==0 to get something
that's true only with -std. */
int osf4_cc_array ['\x00' == 0 ? 1 : -1];
/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters
inside strings and character constants. */
#define FOO(x) 'x'
int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1];
int test (int i, double x);
struct s1 {int (*f) (int a);};
struct s2 {int (*f) (double a);};
int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int);
int argc;
char **argv;
int
main ()
{
return f (e, argv, 0) != argv[0] || f (e, argv, 1) != argv[1];
;
return 0;
}
_ACEOF
for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \
-Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__"
do
CC="$ac_save_CC $ac_arg"
if ac_fn_c_try_compile "$LINENO"; then :
ac_cv_prog_cc_c89=$ac_arg
fi
rm -f core conftest.err conftest.$ac_objext
test "x$ac_cv_prog_cc_c89" != "xno" && break
done
rm -f conftest.$ac_ext
CC=$ac_save_CC
fi
# AC_CACHE_VAL
case "x$ac_cv_prog_cc_c89" in
x)
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5
$as_echo "none needed" >&6; } ;;
xno)
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5
$as_echo "unsupported" >&6; } ;;
*)
CC="$CC $ac_cv_prog_cc_c89"
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5
$as_echo "$ac_cv_prog_cc_c89" >&6; } ;;
esac
if test "x$ac_cv_prog_cc_c89" != xno; then :
fi
ac_ext=c
ac_cpp='$CPP $CPPFLAGS'
ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5'
ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5'
ac_compiler_gnu=$ac_cv_c_compiler_gnu
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for __gmpz_init in -lgmp" >&5
$as_echo_n "checking for __gmpz_init in -lgmp... " >&6; }
if ${ac_cv_lib_gmp___gmpz_init+:} false; then :
$as_echo_n "(cached) " >&6
else
ac_check_lib_save_LIBS=$LIBS
LIBS="-lgmp $LIBS"
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
/* Override any GCC internal prototype to avoid an error.
Use char because int might match the return type of a GCC
builtin and then its argument prototype would still apply. */
#ifdef __cplusplus
extern "C"
#endif
char __gmpz_init ();
int
main ()
{
return __gmpz_init ();
;
return 0;
}
_ACEOF
if ac_fn_c_try_link "$LINENO"; then :
ac_cv_lib_gmp___gmpz_init=yes
else
ac_cv_lib_gmp___gmpz_init=no
fi
rm -f core conftest.err conftest.$ac_objext \
conftest$ac_exeext conftest.$ac_ext
LIBS=$ac_check_lib_save_LIBS
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_gmp___gmpz_init" >&5
$as_echo "$ac_cv_lib_gmp___gmpz_init" >&6; }
if test "x$ac_cv_lib_gmp___gmpz_init" = xyes; then :
gmp=yes
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: GNU MP not found" >&5
$as_echo "GNU MP not found" >&6; }
gmp=no
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for mpfr_add in -lmpfr" >&5
$as_echo_n "checking for mpfr_add in -lmpfr... " >&6; }
if ${ac_cv_lib_mpfr_mpfr_add+:} false; then :
$as_echo_n "(cached) " >&6
else
ac_check_lib_save_LIBS=$LIBS
LIBS="-lmpfr $LIBS"
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
/* Override any GCC internal prototype to avoid an error.
Use char because int might match the return type of a GCC
builtin and then its argument prototype would still apply. */
#ifdef __cplusplus
extern "C"
#endif
char mpfr_add ();
int
main ()
{
return mpfr_add ();
;
return 0;
}
_ACEOF
if ac_fn_c_try_link "$LINENO"; then :
ac_cv_lib_mpfr_mpfr_add=yes
else
ac_cv_lib_mpfr_mpfr_add=no
fi
rm -f core conftest.err conftest.$ac_objext \
conftest$ac_exeext conftest.$ac_ext
LIBS=$ac_check_lib_save_LIBS
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_mpfr_mpfr_add" >&5
$as_echo "$ac_cv_lib_mpfr_mpfr_add" >&6; }
if test "x$ac_cv_lib_mpfr_mpfr_add" = xyes; then :
mpfr=yes
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: MPFR not found" >&5
$as_echo "MPFR not found" >&6; }
mpfr=no
fi
# Workaround to solve an issue with ocamlbuild and C libraries. # Workaround to solve an issue with ocamlbuild and C libraries.
# oCFLAGS="$CFLAGS" # oCFLAGS="$CFLAGS"
...@@ -1856,7 +2849,7 @@ _ACEOF ...@@ -1856,7 +2849,7 @@ _ACEOF
# Instanciation # Instanciation
ac_config_files="$ac_config_files Makefile src/Makefile src/version.ml" ac_config_files="$ac_config_files Makefile src/Makefile src/version.ml test/test-compile.sh"
cat >confcache <<\_ACEOF cat >confcache <<\_ACEOF
...@@ -2401,7 +3394,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 ...@@ -2401,7 +3394,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
# report actual input values of CONFIG_FILES etc. instead of their # report actual input values of CONFIG_FILES etc. instead of their
# values after options handling. # values after options handling.
ac_log=" ac_log="
This file was extended by lustrec $as_me 1.1-Unversioned directory, which was This file was extended by lustrec $as_me 1.3- 55, which was
generated by GNU Autoconf 2.69. Invocation command line was generated by GNU Autoconf 2.69. Invocation command line was
CONFIG_FILES = $CONFIG_FILES CONFIG_FILES = $CONFIG_FILES
...@@ -2454,7 +3447,7 @@ _ACEOF ...@@ -2454,7 +3447,7 @@ _ACEOF
cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`" ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
ac_cs_version="\\ ac_cs_version="\\
lustrec config.status 1.1-Unversioned directory lustrec config.status 1.3- 55
configured by $0, generated by GNU Autoconf 2.69, configured by $0, generated by GNU Autoconf 2.69,
with options \\"\$ac_cs_config\\" with options \\"\$ac_cs_config\\"
...@@ -2567,6 +3560,7 @@ do ...@@ -2567,6 +3560,7 @@ do
"Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;; "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;;
"src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;; "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;;
"src/version.ml") CONFIG_FILES="$CONFIG_FILES src/version.ml" ;; "src/version.ml") CONFIG_FILES="$CONFIG_FILES src/version.ml" ;;
"test/test-compile.sh") CONFIG_FILES="$CONFIG_FILES test/test-compile.sh" ;;
*) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
esac esac
...@@ -3019,3 +4013,27 @@ fi ...@@ -3019,3 +4013,27 @@ fi
# summary # summary
{ $as_echo "$as_me:${as_lineno-$LINENO}: ******** Configuration ********" >&5
$as_echo "$as_me: ******** Configuration ********" >&6;}
{ $as_echo "$as_me:${as_lineno-$LINENO}: bin path: $prefix/bin" >&5
$as_echo "$as_me: bin path: $prefix/bin" >&6;}
{ $as_echo "$as_me:${as_lineno-$LINENO}: include path: $prefix/include" >&5
$as_echo "$as_me: include path: $prefix/include" >&6;}
{ $as_echo "$as_me:${as_lineno-$LINENO}: ******** Plugins ********" >&5
$as_echo "$as_me: ******** Plugins ********" >&6;}
if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
{ $as_echo "$as_me:${as_lineno-$LINENO}: -mpfr option enable" >&5
$as_echo "$as_me: -mpfr option enable" >&6;}
else
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: MPFR option cannot be activated. Requires GMP and MPFR libs" >&5
$as_echo "$as_me: WARNING: MPFR option cannot be activated. Requires GMP and MPFR libs" >&2;}
fi
{ $as_echo "$as_me:${as_lineno-$LINENO}: " >&5
$as_echo "$as_me: " >&6;}
{ $as_echo "$as_me:${as_lineno-$LINENO}: ******** Configuration ********" >&5
$as_echo "$as_me: ******** Configuration ********" >&6;}
autom4te.cache/requests
+ 45
− 45
View file @ 9f77bff7
...@@ -14,63 +14,63 @@ ...@@ -14,63 +14,63 @@
'configure.ac' 'configure.ac'
], ],
{ {
'm4_pattern_allow' => 1,
'AC_CANONICAL_SYSTEM' => 1,
'AM_PROG_F77_C_O' => 1,
'AC_FC_PP_DEFINE' => 1,
'AM_INIT_AUTOMAKE' => 1,
'LT_CONFIG_LTDL_DIR' => 1,
'AC_LIBSOURCE' => 1,
'AM_POT_TOOLS' => 1,
'AC_CONFIG_LINKS' => 1,
'LT_INIT' => 1,
'_AM_COND_IF' => 1,
'AM_MAKEFILE_INCLUDE' => 1,
'_AM_COND_ELSE' => 1,
'AC_CONFIG_SUBDIRS' => 1,
'AC_SUBST' => 1,
'AC_DEFINE_TRACE_LITERAL' => 1,
'm4_include' => 1,
'm4_pattern_forbid' => 1,
'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
'_AM_MAKEFILE_INCLUDE' => 1, '_AM_MAKEFILE_INCLUDE' => 1,
'AM_PROG_AR' => 1, 'AC_CANONICAL_SYSTEM' => 1,
'LT_SUPPORTED_TAG' => 1, 'AC_INIT' => 1,
'AC_CONFIG_AUX_DIR' => 1,
'AC_CONFIG_LIBOBJ_DIR' => 1,
'AC_PROG_LIBTOOL' => 1,
'AC_FC_PP_SRCEXT' => 1,
'AC_CANONICAL_BUILD' => 1,
'AM_SILENT_RULES' => 1,
'AC_CONFIG_FILES' => 1, 'AC_CONFIG_FILES' => 1,
'_m4_warn' => 1, '_m4_warn' => 1,
'AC_FC_SRCEXT' => 1, 'm4_sinclude' => 1,
'AC_INIT' => 1, 'm4_pattern_forbid' => 1,
'_AM_COND_IF' => 1,
'AH_OUTPUT' => 1,
'_AM_COND_ENDIF' => 1,
'AM_PROG_AR' => 1,
'AC_CANONICAL_TARGET' => 1, 'AC_CANONICAL_TARGET' => 1,
'AC_CANONICAL_HOST' => 1, 'LT_SUPPORTED_TAG' => 1,
'AC_FC_FREEFORM' => 1, 'AC_FC_FREEFORM' => 1,
'AH_OUTPUT' => 1, 'AM_PROG_F77_C_O' => 1,
'_LT_AC_TAGCONFIG' => 1,
'_AM_SUBST_NOTMAKE' => 1, '_AM_SUBST_NOTMAKE' => 1,
'm4_sinclude' => 1, 'AC_SUBST' => 1,
'AM_MAINTAINER_MODE' => 1, 'AM_MAKEFILE_INCLUDE' => 1,
'sinclude' => 1, 'LT_INIT' => 1,
'_AM_COND_ENDIF' => 1, 'AC_FC_PP_DEFINE' => 1,
'AC_PROG_LIBTOOL' => 1,
'AM_XGETTEXT_OPTION' => 1, 'AM_XGETTEXT_OPTION' => 1,
'AC_DEFINE_TRACE_LITERAL' => 1,
'AC_SUBST_TRACE' => 1, 'AC_SUBST_TRACE' => 1,
'_LT_AC_TAGCONFIG' => 1,
'AM_PROG_CXX_C_O' => 1,
'include' => 1,
'AM_GNU_GETTEXT' => 1,
'AC_CONFIG_HEADERS' => 1, 'AC_CONFIG_HEADERS' => 1,
'sinclude' => 1,
'AC_CONFIG_LIBOBJ_DIR' => 1,
'AC_LIBSOURCE' => 1,
'AM_POT_TOOLS' => 1,
'AM_GNU_GETTEXT' => 1,
'AM_SILENT_RULES' => 1,
'm4_include' => 1,
'AM_PROG_CC_C_O' => 1,
'AC_CANONICAL_HOST' => 1,
'include' => 1,
'AM_INIT_AUTOMAKE' => 1,
'AM_AUTOMAKE_VERSION' => 1,
'AM_PATH_GUILE' => 1,
'AC_REQUIRE_AUX_FILE' => 1,
'AM_ENABLE_MULTILIB' => 1,
'AC_CANONICAL_BUILD' => 1,
'AM_NLS' => 1, 'AM_NLS' => 1,
'AC_FC_PP_SRCEXT' => 1,
'AC_CONFIG_LINKS' => 1,
'AC_CONFIG_SUBDIRS' => 1,
'AC_FC_SRCEXT' => 1,
'AM_PROG_CXX_C_O' => 1,
'AM_PROG_MOC' => 1,
'm4_pattern_allow' => 1,
'AM_CONDITIONAL' => 1, 'AM_CONDITIONAL' => 1,
'AM_PROG_FC_C_O' => 1, 'AM_PROG_FC_C_O' => 1,
'AC_REQUIRE_AUX_FILE' => 1, 'LT_CONFIG_LTDL_DIR' => 1,
'AM_PROG_MOC' => 1, 'AM_MAINTAINER_MODE' => 1,
'AM_ENABLE_MULTILIB' => 1, '_AM_COND_ELSE' => 1,
'AM_AUTOMAKE_VERSION' => 1, 'AC_CONFIG_AUX_DIR' => 1,
'AM_PROG_CC_C_O' => 1, 'AM_GNU_GETTEXT_INTL_SUBDIR' => 1
'AM_PATH_GUILE' => 1
} }
], 'Autom4te::Request' ) ], 'Autom4te::Request' )
); );
......
autom4te.cache/traces.0
+ 17
− 18
View file @ 9f77bff7
...@@ -152,7 +152,7 @@ m4trace:configure.ac:4: -1- m4_pattern_allow([^VERSION_CODENAME$]) ...@@ -152,7 +152,7 @@ m4trace:configure.ac:4: -1- m4_pattern_allow([^VERSION_CODENAME$])
m4trace:configure.ac:28: -1- AC_SUBST([OCAMLGRAPH_PATH]) m4trace:configure.ac:28: -1- AC_SUBST([OCAMLGRAPH_PATH])
m4trace:configure.ac:28: -1- AC_SUBST_TRACE([OCAMLGRAPH_PATH]) m4trace:configure.ac:28: -1- AC_SUBST_TRACE([OCAMLGRAPH_PATH])
m4trace:configure.ac:28: -1- m4_pattern_allow([^OCAMLGRAPH_PATH$]) m4trace:configure.ac:28: -1- m4_pattern_allow([^OCAMLGRAPH_PATH$])
m4trace:configure.ac:30: -1- AC_SUBST([SRC_PATH], [/Users/Teme/Documents/GitHub/onera_lustrec]) m4trace:configure.ac:30: -1- AC_SUBST([SRC_PATH], [/Users/Teme/Documents/GitHub/lustrec])
m4trace:configure.ac:30: -1- AC_SUBST_TRACE([SRC_PATH]) m4trace:configure.ac:30: -1- AC_SUBST_TRACE([SRC_PATH])
m4trace:configure.ac:30: -1- m4_pattern_allow([^SRC_PATH$]) m4trace:configure.ac:30: -1- m4_pattern_allow([^SRC_PATH$])
m4trace:configure.ac:32: -1- AC_SUBST([OCAMLC]) m4trace:configure.ac:32: -1- AC_SUBST([OCAMLC])
...@@ -202,24 +202,23 @@ m4trace:configure.ac:99: -1- AC_SUBST_TRACE([abs_datadir]) ...@@ -202,24 +202,23 @@ m4trace:configure.ac:99: -1- AC_SUBST_TRACE([abs_datadir])
m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$]) m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$])
m4trace:configure.ac:99: -1- AC_DEFINE_TRACE_LITERAL([abs_datadir]) m4trace:configure.ac:99: -1- AC_DEFINE_TRACE_LITERAL([abs_datadir])
m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$]) m4trace:configure.ac:99: -1- m4_pattern_allow([^abs_datadir$])
m4trace:configure.ac:107: -1- AC_CONFIG_FILES([Makefile m4trace:configure.ac:106: -1- AC_CONFIG_FILES([Makefile
src/Makefile src/Makefile
src/myocamlbuild.ml
src/version.ml src/version.ml
test/test-compile.sh test/test-compile.sh
]) ])
m4trace:configure.ac:109: -1- AC_SUBST([LIB@&t@OBJS], [$ac_libobjs]) m4trace:configure.ac:108: -1- AC_SUBST([LIB@&t@OBJS], [$ac_libobjs])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([LIB@&t@OBJS]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([LIB@&t@OBJS])
m4trace:configure.ac:109: -1- m4_pattern_allow([^LIB@&t@OBJS$]) m4trace:configure.ac:108: -1- m4_pattern_allow([^LIB@&t@OBJS$])
m4trace:configure.ac:109: -1- AC_SUBST([LTLIBOBJS], [$ac_ltlibobjs]) m4trace:configure.ac:108: -1- AC_SUBST([LTLIBOBJS], [$ac_ltlibobjs])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([LTLIBOBJS]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([LTLIBOBJS])
m4trace:configure.ac:109: -1- m4_pattern_allow([^LTLIBOBJS$]) m4trace:configure.ac:108: -1- m4_pattern_allow([^LTLIBOBJS$])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_builddir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_builddir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_build_prefix]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_build_prefix])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([srcdir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([srcdir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_srcdir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_srcdir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([top_srcdir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([top_srcdir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_top_srcdir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_top_srcdir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([builddir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([builddir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_builddir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_builddir])
m4trace:configure.ac:109: -1- AC_SUBST_TRACE([abs_top_builddir]) m4trace:configure.ac:108: -1- AC_SUBST_TRACE([abs_top_builddir])
include/math.smt2 0 → 100644
+ 6
− 0
View file @ 9f77bff7
(declare-rel cbrt (Real Real))
(declare-rel ceil (Real Real))
(declare-rel erf (Real Real))
(declare-rel fabs (Real Real))
(declare-rel pow (Real Real Real))
(declare-rel sqrt (Real Real))
src/backends/Horn/horn_backend_common.ml
+ 6
− 6
View file @ 9f77bff7
...@@ -69,7 +69,7 @@ let get_machine machines node_name = ...@@ -69,7 +69,7 @@ let get_machine machines node_name =
let local_memory_vars machines machine = let local_memory_vars machines machine =
rename_machine_list machine.mname.node_id machine.mmemory rename_machine_list machine.mname.node_id machine.mmemory
let instances_memory_vars ?(without_arrow=false) machines machine = let instances_memory_vars ?(without_arrow=false) machines machine =
let rec aux fst prefix m = let rec aux fst prefix m =
( (
...@@ -81,10 +81,10 @@ let instances_memory_vars ?(without_arrow=false) machines machine = ...@@ -81,10 +81,10 @@ let instances_memory_vars ?(without_arrow=false) machines machine =
List.fold_left (fun accu (id, (n, _)) -> List.fold_left (fun accu (id, (n, _)) ->
let name = node_name n in let name = node_name n in
if without_arrow && name = "_arrow" then if without_arrow && name = "_arrow" then
accu accu
else else
let machine_n = get_machine machines name in let machine_n = get_machine machines name in
( aux false (concat prefix ( aux false (concat prefix
(if fst then id else concat m.mname.node_id id)) (if fst then id else concat m.mname.node_id id))
machine_n ) @ accu machine_n ) @ accu
) [] (m.minstances) ) [] (m.minstances)
...@@ -101,16 +101,16 @@ let inout_vars machines m = ...@@ -101,16 +101,16 @@ let inout_vars machines m =
let step_vars machines m = let step_vars machines m =
(inout_vars machines m) (inout_vars machines m)
@ (rename_current_list (full_memory_vars machines m)) @ (rename_current_list (full_memory_vars machines m))
@ (rename_next_list (full_memory_vars machines m)) @ (rename_next_list (full_memory_vars machines m))
let step_vars_m_x machines m = let step_vars_m_x machines m =
(inout_vars machines m) (inout_vars machines m)
@ (rename_mid_list (full_memory_vars machines m)) @ (rename_mid_list (full_memory_vars machines m))
@ (rename_next_list (full_memory_vars machines m)) @ (rename_next_list (full_memory_vars machines m))
let reset_vars machines m = let reset_vars machines m =
(rename_current_list (full_memory_vars machines m)) (rename_current_list (full_memory_vars machines m))
@ (rename_mid_list (full_memory_vars machines m)) @ (rename_mid_list (full_memory_vars machines m))
......
src/backends/Horn/horn_backend_traces.ml
+ 19
− 19
View file @ 9f77bff7
...@@ -39,7 +39,7 @@ let compute_mems machines m = ...@@ -39,7 +39,7 @@ let compute_mems machines m =
(* We extract the annotation dealing with traceability *) (* We extract the annotation dealing with traceability *)
let machines_traces machines = let machines_traces machines =
List.map (fun m -> List.map (fun m ->
let traces : (ident * expr) list= let traces : (ident * expr) list=
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
...@@ -61,12 +61,12 @@ let machines_traces machines = ...@@ -61,12 +61,12 @@ let machines_traces machines =
m, traces m, traces
) machines ) machines
let memories_old machines m = let memories_old machines m =
List.map (fun (p, v) -> List.map (fun (p, v) ->
let machine = match p with | [] -> m | (_,m')::_ -> m' in let machine = match p with | [] -> m | (_,m')::_ -> m' in
let traces = List.assoc machine (machines_traces machines) in let traces = List.assoc machine (machines_traces machines) in
if List.mem_assoc v.var_id traces then if List.mem_assoc v.var_id traces then
( (
(* We take the expression associated to variable v in the trace (* We take the expression associated to variable v in the trace
info *) info *)
...@@ -75,20 +75,20 @@ let memories_old machines m = ...@@ -75,20 +75,20 @@ let memories_old machines m =
Printers.pp_expr (List.assoc v.var_id traces); *) Printers.pp_expr (List.assoc v.var_id traces); *)
p, List.assoc v.var_id traces p, List.assoc v.var_id traces
) )
else else
begin begin
(* We keep the variable as is: we create an expression v *) (* We keep the variable as is: we create an expression v *)
(* eprintf "Unable to found variable %a in traces (%a)@." pp_var v (* eprintf "Unable to found variable %a in traces (%a)@." pp_var v
(Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
traces); *) traces); *)
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
end end
) (compute_mems machines m) ) (compute_mems machines m)
let memories_next machines m = (* We remove the topest pre in each expression *) let memories_next machines m = (* We remove the topest pre in each expression *)
List.map List.map
(fun (prefix, ee) -> (fun (prefix, ee) ->
...@@ -102,15 +102,15 @@ let memories_next machines m = (* We remove the topest pre in each expression * ...@@ -102,15 +102,15 @@ let memories_next machines m = (* We remove the topest pre in each expression *
Printers.pp_expr ee; Printers.pp_expr ee;
assert false) assert false)
(memories_old machines m) (memories_old machines m)
let pp_prefix_rev fmt prefix = let pp_prefix_rev fmt prefix =
Utils.fprintf_list ~sep:"." Utils.fprintf_list ~sep:"."
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
fmt fmt
(List.rev prefix) (List.rev prefix)
let traces_file fmt basename prog machines = let traces_file fmt basename prog machines =
fprintf fmt "<?xml version=\"1.0\"?>@."; fprintf fmt "<?xml version=\"1.0\"?>@.";
...@@ -120,10 +120,10 @@ let traces_file fmt basename prog machines = ...@@ -120,10 +120,10 @@ let traces_file fmt basename prog machines =
let pp_var = pp_horn_var m in let pp_var = pp_horn_var m in
let memories_old = memories_old machines m in let memories_old = memories_old machines m in
let memories_next = memories_next machines m in let memories_next = memories_next machines m in
(* fprintf fmt "; Node %s@." m.mname.node_id; *) (* fprintf fmt "; Node %s@." m.mname.node_id; *)
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
...@@ -135,11 +135,11 @@ let traces_file fmt basename prog machines = ...@@ -135,11 +135,11 @@ let traces_file fmt basename prog machines =
(Utils.fprintf_list ~sep:" | " pp_var) output_vars (Utils.fprintf_list ~sep:" | " pp_var) output_vars
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars (Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
let init_local_vars = let init_local_vars =
(rename_next_list
(rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false)) (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
in in
let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in
...@@ -160,7 +160,7 @@ let traces_file fmt basename prog machines = ...@@ -160,7 +160,7 @@ let traces_file fmt basename prog machines =
fprintf fmt "@]@ </Node>"; fprintf fmt "@]@ </Node>";
)) (List.rev machines); )) (List.rev machines);
fprintf fmt "</Traces>@." fprintf fmt "</Traces>@."
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt
"%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
......
src/version.ml
+ 2
− 2
View file @ 9f77bff7
let number = "1.1-Unversioned directory" let number = "1.3- 55"
let codename ="@VERSION_CODENAME@" let codename ="Xia/Zhong-Kang-dev"
let prefix = "/usr/local" let prefix = "/usr/local"
......
test/test-compile.sh
+ 2
− 43
View file @ 9f77bff7
...@@ -5,21 +5,18 @@ eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@") ...@@ -5,21 +5,18 @@ eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
declare c i w h a v declare c i w h a v
declare -a files declare -a files
SRC_PREFIX=/Users/Teme/Documents/GitHub/onera_lustrec-tests/ SRC_PREFIX=/Users/Teme/Documents/GitHub/lustrec-tests/
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler #SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
NOW=`date "+%y%m%d%H%M"` NOW=`date "+%y%m%d%H%M"`
report=`pwd`/report-1.3- 459-$NOW report=`pwd`/report-1.3- 55-$NOW
LUSTREC=lustrec LUSTREC=lustrec
mkdir -p build mkdir -p build
build=`pwd`"/build" build=`pwd`"/build"
gcc_compile() { gcc_compile() {
<<<<<<< HEAD
=======
if [ $verbose -gt 1 ]; then if [ $verbose -gt 1 ]; then
echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null" echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
fi fi
>>>>>>> onera_master
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null; gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
if [ $? -ne 0 ]; then if [ $? -ne 0 ]; then
rgcc="INVALID"; rgcc="INVALID";
...@@ -29,12 +26,9 @@ gcc_compile() { ...@@ -29,12 +26,9 @@ gcc_compile() {
} }
lustrec_compile() { lustrec_compile() {
<<<<<<< HEAD
=======
if [ $verbose -gt 1 ]; then if [ $verbose -gt 1 ]; then
echo "$LUSTREC $@" echo "$LUSTREC $@"
fi fi
>>>>>>> onera_master
$LUSTREC "$@"; $LUSTREC "$@";
if [ $? -ne 0 ]; then if [ $? -ne 0 ]; then
rlustrec="INVALID"; rlustrec="INVALID";
...@@ -130,34 +124,6 @@ inline_compile_with_check () { ...@@ -130,34 +124,6 @@ inline_compile_with_check () {
fi fi
dir=${SRC_PREFIX}/`dirname "$file"` dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null pushd $dir > /dev/null
<<<<<<< HEAD
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
pushd $build > /dev/null
gcc_compile "$name"
popd > /dev/null
# Cheching witness
pushd $build > /dev/null
lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
popd > /dev/null
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
rinlining="VALID";
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
rinlining="ERROR";
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
rinlining="UNKNOWN";
else
rinlining="INVALID/TIMEOUT"
fi
if [ $verbose -gt 0 ]; then
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
else
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
fi
popd > /dev/null
=======
if [ "$main" != "" ]; then if [ "$main" != "" ]; then
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext; lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
...@@ -204,7 +170,6 @@ inline_compile_with_check () { ...@@ -204,7 +170,6 @@ inline_compile_with_check () {
else else
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN" echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
fi fi
>>>>>>> onera_master
done < $file_list done < $file_list
} }
...@@ -221,15 +186,9 @@ check_prop () { ...@@ -221,15 +186,9 @@ check_prop () {
# Checking horn backend # Checking horn backend
if [ "$main" != "" ]; then if [ "$main" != "" ]; then
<<<<<<< HEAD
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
else
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
=======
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus"; lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
else else
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus" lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
>>>>>>> onera_master
fi fi
# echo "z3 $build/$name".smt2 # echo "z3 $build/$name".smt2
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment