Update to compile with the Intel compiler.
This commit is contained in:
parent
7998fff056
commit
1d58493be3
13 changed files with 87 additions and 53 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -21,3 +21,4 @@ stdout
|
||||||
*.orig
|
*.orig
|
||||||
*.rej
|
*.rej
|
||||||
*.old
|
*.old
|
||||||
|
TAGS
|
||||||
|
|
|
||||||
22
ChangeLog
22
ChangeLog
|
|
@ -1,3 +1,25 @@
|
||||||
|
2008-12-11 Guillaume SADEGH <sadegh@lrde.epita.fr>
|
||||||
|
|
||||||
|
Update to compile with the Intel compiler.
|
||||||
|
|
||||||
|
* m4/intel.m4: New file.
|
||||||
|
* configure.ac: Update.
|
||||||
|
* src/tgbaalgos/emptiness.cc (tgba_run): Modify s.s->clone() in
|
||||||
|
i->s->clone().
|
||||||
|
* src/misc/optionmap.hh, src/misc/optionmap.cc: Remove the extra
|
||||||
|
`;' after the namespace.
|
||||||
|
* src/tgbaalgos/tau03opt.cc
|
||||||
|
(tau03_opt_search::add_new_state): Remove unreferenced method.
|
||||||
|
* src/tgbaalgos/ltl2tgba_fm.cc
|
||||||
|
(translate_dict::dump): Remove unreferenced method.
|
||||||
|
* src/tgbaalgos/lbtt.cc
|
||||||
|
(acceptance_cond_splitter::count): Remove unreferenced method.
|
||||||
|
* src/tgba/tgbabddconcreteproduct.cc
|
||||||
|
(tgba_bdd_product_factory::get_dict): Remove unreferenced method.
|
||||||
|
* src/ltlvisit/syntimpl.cc
|
||||||
|
(eventual_universal_visitor::recurse): Remove unreferenced method.
|
||||||
|
* src/tgbaalgos/reductgba_sim.cc: Reindent.
|
||||||
|
|
||||||
2008-12-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2008-12-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Compute more statistics about SCCs.
|
Compute more statistics about SCCs.
|
||||||
|
|
|
||||||
|
|
@ -51,6 +51,7 @@ AC_CHECK_FUNCS([srand48 drand48])
|
||||||
AC_LIBTOOL_WIN32_DLL
|
AC_LIBTOOL_WIN32_DLL
|
||||||
AC_PROG_LIBTOOL
|
AC_PROG_LIBTOOL
|
||||||
|
|
||||||
|
spot_INTEL
|
||||||
CF_GXX_WARNINGS
|
CF_GXX_WARNINGS
|
||||||
adl_ENABLE_DEBUG
|
adl_ENABLE_DEBUG
|
||||||
ad_GCC_OPTIM
|
ad_GCC_OPTIM
|
||||||
|
|
|
||||||
54
m4/intel.m4
Normal file
54
m4/intel.m4
Normal file
|
|
@ -0,0 +1,54 @@
|
||||||
|
|
||||||
|
|
||||||
|
dnl Adapted from the predefined _AC_LANG_COMPILER_GNU.
|
||||||
|
m4_define([_AC_LANG_COMPILER_INTEL],
|
||||||
|
[AC_CACHE_CHECK([whether we are using the INTEL _AC_LANG compiler],
|
||||||
|
[ac_cv_[]_AC_LANG_ABBREV[]_compiler_intel],
|
||||||
|
[
|
||||||
|
_AC_COMPILE_IFELSE([AC_LANG_PROGRAM([], [[#ifndef __INTEL_COMPILER
|
||||||
|
choke me
|
||||||
|
#endif
|
||||||
|
]])],
|
||||||
|
[ac_compiler_intel=yes],
|
||||||
|
[ac_compiler_intel=no])
|
||||||
|
ac_cv_[]_AC_LANG_ABBREV[]_compiler_intel=$ac_compiler_intel
|
||||||
|
])])# _AC_LANG_COMPILER_INTEL
|
||||||
|
|
||||||
|
dnl The list of warnings which must be disabled for Spot.
|
||||||
|
m4_define([_INTEL_IGNORE_WARNINGS],
|
||||||
|
[ 69 dnl Warn when an enum value is used as an int, without any
|
||||||
|
dnl explicit cast.
|
||||||
|
279 dnl Warn when a constant expression is used in a control statement.
|
||||||
|
654 dnl Warn when a child does not overload all virtual members of his
|
||||||
|
dnl parents.
|
||||||
|
913 dnl Warn when multibyte character are used (for example "Büchi").
|
||||||
|
1125 dnl Warn when a child member hides a parent member.
|
||||||
|
]) # _INTEL_IGNORE_WARNINGS
|
||||||
|
|
||||||
|
dnl Add extra flags when icpc is used.
|
||||||
|
AC_DEFUN([spot_INTEL],
|
||||||
|
[_AC_LANG_COMPILER_INTEL
|
||||||
|
AC_CACHE_CHECK([to add extra CXXFLAGS for the INTEL C++ compiler],
|
||||||
|
[ac_cv_intel_cxxflags],
|
||||||
|
[ dnl
|
||||||
|
if test x"$ac_compiler_intel" = x"yes"; then
|
||||||
|
disabled_warnings=''
|
||||||
|
for warning in _INTEL_IGNORE_WARNINGS; do
|
||||||
|
disabled_warnings="$disabled_warnings,$warning"
|
||||||
|
done
|
||||||
|
|
||||||
|
# remove the extra "," and extra whitespaces.
|
||||||
|
disabled_warnings=`echo "$disabled_warnings" | sed "s/^,//;s/[[:space:]]//g"`
|
||||||
|
|
||||||
|
INTEL_CXXFLAGS="-w1 -Werror -wd${disabled_warnings}"
|
||||||
|
|
||||||
|
# Even if the icpc preprocessor defines __GNUC__, it is not a GNU compiler.
|
||||||
|
GXX=
|
||||||
|
CXXFLAGS="$CXXFLAGS $INTEL_CXXFLAGS"
|
||||||
|
|
||||||
|
[ac_cv_intel_cxxflags="$INTEL_CXXFLAGS"]
|
||||||
|
else
|
||||||
|
[ac_cv_intel_cxxflags="no extra flags"]
|
||||||
|
fi])
|
||||||
|
AC_SUBST([INTEL_CXXFLAGS])
|
||||||
|
]) # spot_INTEL
|
||||||
|
|
@ -301,16 +301,6 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
|
||||||
recurse(const formula* f1, const formula* f2)
|
|
||||||
{
|
|
||||||
if (f1 == f2)
|
|
||||||
return true;
|
|
||||||
inf_right_recurse_visitor v(f2);
|
|
||||||
const_cast<formula*>(f1)->accept(v);
|
|
||||||
return v.result();
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
bool result_; /* true if f < f1, false otherwise. */
|
bool result_; /* true if f < f1, false otherwise. */
|
||||||
const formula* f;
|
const formula* f;
|
||||||
|
|
|
||||||
|
|
@ -157,4 +157,4 @@ namespace spot
|
||||||
os << "\"" << it->first << "\" = " << it->second << std::endl;
|
os << "\"" << it->first << "\" = " << it->second << std::endl;
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
};
|
}
|
||||||
|
|
|
||||||
|
|
@ -82,6 +82,6 @@ namespace spot
|
||||||
private:
|
private:
|
||||||
std::map<std::string, int> options_;
|
std::map<std::string, int> options_;
|
||||||
};
|
};
|
||||||
};
|
}
|
||||||
|
|
||||||
#endif // SPOT_MISC_OPTIONMAP_HH
|
#endif // SPOT_MISC_OPTIONMAP_HH
|
||||||
|
|
|
||||||
|
|
@ -56,12 +56,6 @@ namespace spot
|
||||||
return data_;
|
return data_;
|
||||||
}
|
}
|
||||||
|
|
||||||
bdd_dict*
|
|
||||||
get_dict() const
|
|
||||||
{
|
|
||||||
return dict_;
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd
|
bdd
|
||||||
get_init_state() const
|
get_init_state() const
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -50,13 +50,13 @@ namespace spot
|
||||||
for (steps::const_iterator i = run.prefix.begin();
|
for (steps::const_iterator i = run.prefix.begin();
|
||||||
i != run.prefix.end(); ++i)
|
i != run.prefix.end(); ++i)
|
||||||
{
|
{
|
||||||
step s = { s.s->clone(), i->label, i->acc };
|
step s = { i->s->clone(), i->label, i->acc };
|
||||||
prefix.push_back(s);
|
prefix.push_back(s);
|
||||||
}
|
}
|
||||||
for (steps::const_iterator i = run.cycle.begin();
|
for (steps::const_iterator i = run.cycle.begin();
|
||||||
i != run.cycle.end(); ++i)
|
i != run.cycle.end(); ++i)
|
||||||
{
|
{
|
||||||
step s = { s.s->clone(), i->label, i->acc };
|
step s = { i->s->clone(), i->label, i->acc };
|
||||||
cycle.push_back(s);
|
cycle.push_back(s);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -62,12 +62,6 @@ namespace spot
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned
|
|
||||||
count() const
|
|
||||||
{
|
|
||||||
return sm.size();
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
private:
|
||||||
typedef std::map<bdd, unsigned, bdd_less_than> split_map;
|
typedef std::map<bdd, unsigned, bdd_less_than> split_map;
|
||||||
split_map sm;
|
split_map sm;
|
||||||
|
|
|
||||||
|
|
@ -117,21 +117,6 @@ namespace spot
|
||||||
return num;
|
return num;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream&
|
|
||||||
dump(std::ostream& os) const
|
|
||||||
{
|
|
||||||
fv_map::const_iterator fi;
|
|
||||||
os << "Next Variables:" << std::endl;
|
|
||||||
for (fi = next_map.begin(); fi != next_map.end(); ++fi)
|
|
||||||
{
|
|
||||||
os << " " << fi->second << ": Next[";
|
|
||||||
fi->first->to_string(os) << "]" << std::endl;
|
|
||||||
}
|
|
||||||
os << "Shared Dict:" << std::endl;
|
|
||||||
dict->dump(os);
|
|
||||||
return os;
|
|
||||||
}
|
|
||||||
|
|
||||||
formula*
|
formula*
|
||||||
var_to_formula(int var) const
|
var_to_formula(int var) const
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -276,16 +276,16 @@ namespace spot
|
||||||
|
|
||||||
void
|
void
|
||||||
parity_game_graph::process_state(const state* s,
|
parity_game_graph::process_state(const state* s,
|
||||||
int ,
|
int,
|
||||||
tgba_succ_iterator*)
|
tgba_succ_iterator*)
|
||||||
{
|
{
|
||||||
tgba_state_.push_back(s);
|
tgba_state_.push_back(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
parity_game_graph::process_link(int ,
|
parity_game_graph::process_link(int,
|
||||||
int ,
|
int,
|
||||||
const tgba_succ_iterator*)
|
const tgba_succ_iterator*)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -530,13 +530,6 @@ namespace spot
|
||||||
&(ic->second.first), &(ic->second.second));
|
&(ic->second.first), &(ic->second.second));
|
||||||
}
|
}
|
||||||
|
|
||||||
void add_new_state(const state* s, color c)
|
|
||||||
{
|
|
||||||
assert(hc.find(s)==hc.end() && h.find(s)==h.end());
|
|
||||||
assert(c != CYAN);
|
|
||||||
h.insert(std::make_pair(s, std::make_pair(c, bddfalse)));
|
|
||||||
}
|
|
||||||
|
|
||||||
void add_new_state(const state* s, color c, const weight& w)
|
void add_new_state(const state* s, color c, const weight& w)
|
||||||
{
|
{
|
||||||
assert(hc.find(s)==hc.end() && h.find(s)==h.end());
|
assert(hc.find(s)==hc.end() && h.find(s)==h.end());
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue