* HACKING, src/sanity/style.test: NULL is not portable, prohibit it.
* iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/syntimpl.cc: Use 0 instead of NULL.
This commit is contained in:
parent
6e3fd873ba
commit
8e324fa2a2
9 changed files with 87 additions and 79 deletions
|
|
@ -1,4 +1,11 @@
|
||||||
2004-06-01 Alexandre Duret-Lutz <adl@gnu.org>
|
2004-06-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
|
* HACKING, src/sanity/style.test: NULL is not portable, prohibit it.
|
||||||
|
* iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
|
||||||
|
src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
|
||||||
|
src/ltlvisit/syntimpl.cc: Use 0 instead of NULL.
|
||||||
|
|
||||||
|
2004-06-01 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
* src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ...
|
* src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ...
|
||||||
* src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
|
* src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
|
||||||
|
|
|
||||||
42
HACKING
42
HACKING
|
|
@ -172,6 +172,25 @@ Formating
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
* Pointers and references are part of the type, and should be put
|
||||||
|
near the type, not near the variable.
|
||||||
|
|
||||||
|
int* p; // not `int *p;'
|
||||||
|
list& l; // not `list &l;'
|
||||||
|
void* magic(); // not `void *magic();'
|
||||||
|
|
||||||
|
* Do not declare many variables on one line.
|
||||||
|
Use
|
||||||
|
int* p;
|
||||||
|
int* q;
|
||||||
|
instead of
|
||||||
|
int *p, *q;
|
||||||
|
The former declarations also allow you to describe each variable.
|
||||||
|
|
||||||
|
* The include guard for src/somedir/foo.hh is
|
||||||
|
SPOT_SOMEDIR_FOO_HH
|
||||||
|
|
||||||
|
|
||||||
Naming
|
Naming
|
||||||
======
|
======
|
||||||
|
|
||||||
|
|
@ -212,20 +231,15 @@ Naming
|
||||||
|
|
||||||
* C Macros are all uppercase.
|
* C Macros are all uppercase.
|
||||||
|
|
||||||
* Pointers and references are part of the type, and should be put
|
|
||||||
near the type, not near the variable.
|
|
||||||
|
|
||||||
int* p; // not `int *p;'
|
Other style recommandations
|
||||||
list& l; // not `list &l;'
|
===========================
|
||||||
void* magic(); // not `void *magic();'
|
|
||||||
|
|
||||||
* Do not declare many variables on one line.
|
* Do not use the NULL macro, it is not always implemented in a way
|
||||||
Use
|
which is compatible with all pointer types. Always use 0 instead.
|
||||||
int* p;
|
|
||||||
int* q;
|
|
||||||
instead of
|
|
||||||
int *p, *q;
|
|
||||||
The former declarations also allow you to describe each variable.
|
|
||||||
|
|
||||||
* The include guard for src/somedir/foo.hh is
|
* Limit the scope of local variables by defining them as late as
|
||||||
SPOT_SOMEDIR_FOO_HH
|
possible. Do not reuse a local variables for two different things.
|
||||||
|
|
||||||
|
* Do not systematically initialise local variables with 0 or other
|
||||||
|
meaningless values. This hides errors to valgrind.
|
||||||
|
|
|
||||||
|
|
@ -938,7 +938,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
if (spot_inclusion(old_state->left(), new_state->left()))
|
if (spot_inclusion(old_state->left(), new_state->left()))
|
||||||
{
|
{
|
||||||
State* succ_tgba_ = NULL;
|
State* succ_tgba_ = 0;
|
||||||
size_t size_tgba_ = 0;
|
size_t size_tgba_ = 0;
|
||||||
succ_queue& queue = todo.top().second;
|
succ_queue& queue = todo.top().second;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -77,7 +77,7 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
spot::ltl::parse_error_list p1;
|
spot::ltl::parse_error_list p1;
|
||||||
spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
|
spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
|
||||||
spot::ltl::formula* f2 = NULL;
|
spot::ltl::formula* f2 = 0;
|
||||||
|
|
||||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
||||||
return 2;
|
return 2;
|
||||||
|
|
@ -119,7 +119,7 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
bool red = (length_f1_after < length_f1_before);
|
bool red = (length_f1_after < length_f1_before);
|
||||||
std::string f2s = "";
|
std::string f2s = "";
|
||||||
if (f2 != NULL)
|
if (f2)
|
||||||
{
|
{
|
||||||
ftmp1 = f2;
|
ftmp1 = f2;
|
||||||
f2 = unabbreviate_logic(f2);
|
f2 = unabbreviate_logic(f2);
|
||||||
|
|
@ -170,7 +170,7 @@ main(int argc, char** argv)
|
||||||
}
|
}
|
||||||
|
|
||||||
spot::ltl::destroy(f1);
|
spot::ltl::destroy(f1);
|
||||||
if (f2 != NULL)
|
if (f2)
|
||||||
spot::ltl::destroy(f2);
|
spot::ltl::destroy(f2);
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -47,13 +47,12 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
spot::ltl::parse_error_list p1;
|
spot::ltl::parse_error_list p1;
|
||||||
spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
|
spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
|
||||||
spot::ltl::formula* f2 = NULL;
|
|
||||||
|
|
||||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
||||||
return 2;
|
return 2;
|
||||||
|
|
||||||
spot::ltl::parse_error_list p2;
|
spot::ltl::parse_error_list p2;
|
||||||
f2 = spot::ltl::parse(argv[3], p2);
|
spot::ltl::formula* f2 = spot::ltl::parse(argv[3], p2);
|
||||||
|
|
||||||
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
||||||
return 2;
|
return 2;
|
||||||
|
|
|
||||||
|
|
@ -90,9 +90,9 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula* f = uo->child();
|
formula* f = uo->child();
|
||||||
result_ = basic_reduce(f);
|
result_ = basic_reduce(f);
|
||||||
multop* mo = NULL;
|
multop* mo = 0;
|
||||||
unop* u = NULL;
|
unop* u = 0;
|
||||||
binop* bo = NULL;
|
binop* bo = 0;
|
||||||
switch (uo->op())
|
switch (uo->op())
|
||||||
{
|
{
|
||||||
case unop::Not:
|
case unop::Not:
|
||||||
|
|
@ -261,9 +261,8 @@ namespace spot
|
||||||
{
|
{
|
||||||
formula* f1 = bo->first();
|
formula* f1 = bo->first();
|
||||||
formula* f2 = bo->second();
|
formula* f2 = bo->second();
|
||||||
formula* ftmp = NULL;
|
unop* fu1;
|
||||||
unop* fu1 = NULL;
|
unop* fu2;
|
||||||
unop* fu2 = NULL;
|
|
||||||
switch (bo->op())
|
switch (bo->op())
|
||||||
{
|
{
|
||||||
case binop::Xor:
|
case binop::Xor:
|
||||||
|
|
@ -301,9 +300,9 @@ namespace spot
|
||||||
(fu1->op() == unop::X) &&
|
(fu1->op() == unop::X) &&
|
||||||
(fu2->op() == unop::X))
|
(fu2->op() == unop::X))
|
||||||
{
|
{
|
||||||
ftmp = binop::instance(binop::U,
|
formula* ftmp = binop::instance(binop::U,
|
||||||
basic_reduce(fu1->child()),
|
basic_reduce(fu1->child()),
|
||||||
basic_reduce(fu2->child()));
|
basic_reduce(fu2->child()));
|
||||||
result_ = unop::instance(unop::X, basic_reduce(ftmp));
|
result_ = unop::instance(unop::X, basic_reduce(ftmp));
|
||||||
destroy(f1);
|
destroy(f1);
|
||||||
destroy(f2);
|
destroy(f2);
|
||||||
|
|
@ -334,9 +333,9 @@ namespace spot
|
||||||
(fu1->op() == unop::X) &&
|
(fu1->op() == unop::X) &&
|
||||||
(fu2->op() == unop::X))
|
(fu2->op() == unop::X))
|
||||||
{
|
{
|
||||||
ftmp = binop::instance(bo->op(),
|
formula* ftmp = binop::instance(bo->op(),
|
||||||
basic_reduce(fu1->child()),
|
basic_reduce(fu1->child()),
|
||||||
basic_reduce(fu2->child()));
|
basic_reduce(fu2->child()));
|
||||||
result_ = unop::instance(unop::X, basic_reduce(ftmp));
|
result_ = unop::instance(unop::X, basic_reduce(ftmp));
|
||||||
destroy(f1);
|
destroy(f1);
|
||||||
destroy(f2);
|
destroy(f2);
|
||||||
|
|
@ -361,27 +360,23 @@ namespace spot
|
||||||
|
|
||||||
multop::vec* tmpX = new multop::vec;
|
multop::vec* tmpX = new multop::vec;
|
||||||
multop::vec* tmpU = new multop::vec;
|
multop::vec* tmpU = new multop::vec;
|
||||||
multop::vec* tmpUright = NULL;
|
|
||||||
multop::vec* tmpR = new multop::vec;
|
multop::vec* tmpR = new multop::vec;
|
||||||
multop::vec* tmpRright = NULL;
|
|
||||||
multop::vec* tmpFG = new multop::vec;
|
multop::vec* tmpFG = new multop::vec;
|
||||||
multop::vec* tmpGF = new multop::vec;
|
multop::vec* tmpGF = new multop::vec;
|
||||||
|
|
||||||
multop::vec* tmpOther = new multop::vec;
|
multop::vec* tmpOther = new multop::vec;
|
||||||
|
|
||||||
formula* ftmp = NULL;
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
for (unsigned i = 0; i < mos; ++i)
|
||||||
res->push_back(basic_reduce(mo->nth(i)));
|
res->push_back(basic_reduce(mo->nth(i)));
|
||||||
|
|
||||||
|
|
||||||
switch (op)
|
switch (op)
|
||||||
{
|
{
|
||||||
case multop::And:
|
case multop::And:
|
||||||
|
|
||||||
for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
|
for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
|
||||||
{
|
{
|
||||||
if (*i == NULL)
|
// FIXME: why would *i be 0 ?
|
||||||
|
if (!*i)
|
||||||
continue;
|
continue;
|
||||||
unop* uo = dynamic_cast<unop*>(*i);
|
unop* uo = dynamic_cast<unop*>(*i);
|
||||||
binop* bo = dynamic_cast<binop*>(*i);
|
binop* bo = dynamic_cast<binop*>(*i);
|
||||||
|
|
@ -408,8 +403,8 @@ namespace spot
|
||||||
if (bo->op() == binop::U)
|
if (bo->op() == binop::U)
|
||||||
{
|
{
|
||||||
// (a U b) & (c U b) = (a & c) U b
|
// (a U b) & (c U b) = (a & c) U b
|
||||||
ftmp = dynamic_cast<binop*>(*i)->second();
|
formula* ftmp = dynamic_cast<binop*>(*i)->second();
|
||||||
tmpUright = new multop::vec;
|
multop::vec* tmpUright = new multop::vec;
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
{
|
{
|
||||||
if (!*j)
|
if (!*j)
|
||||||
|
|
@ -438,8 +433,8 @@ namespace spot
|
||||||
else if (bo->op() == binop::R)
|
else if (bo->op() == binop::R)
|
||||||
{
|
{
|
||||||
// (a R b) & (a R c) = a R (b & c)
|
// (a R b) & (a R c) = a R (b & c)
|
||||||
ftmp = dynamic_cast<binop*>(*i)->first();
|
formula* ftmp = dynamic_cast<binop*>(*i)->first();
|
||||||
tmpRright = new multop::vec;
|
multop::vec* tmpRright = new multop::vec;
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
{
|
{
|
||||||
if (!*j)
|
if (!*j)
|
||||||
|
|
@ -512,8 +507,8 @@ namespace spot
|
||||||
if (bo->op() == binop::U)
|
if (bo->op() == binop::U)
|
||||||
{
|
{
|
||||||
// (a U b) | (a U c) = a U (b | c)
|
// (a U b) | (a U c) = a U (b | c)
|
||||||
ftmp = bo->first();
|
formula* ftmp = bo->first();
|
||||||
tmpUright = new multop::vec;
|
multop::vec* tmpUright = new multop::vec;
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
{
|
{
|
||||||
if (!*j)
|
if (!*j)
|
||||||
|
|
@ -540,8 +535,8 @@ namespace spot
|
||||||
else if (bo->op() == binop::R)
|
else if (bo->op() == binop::R)
|
||||||
{
|
{
|
||||||
// (a R b) | (c R b) = (a | c) R b
|
// (a R b) | (c R b) = (a | c) R b
|
||||||
ftmp = dynamic_cast<binop*>(*i)->second();
|
formula* ftmp = dynamic_cast<binop*>(*i)->second();
|
||||||
tmpRright = new multop::vec;
|
multop::vec* tmpRright = new multop::vec;
|
||||||
for (multop::vec::iterator j = i; j != res->end(); j++)
|
for (multop::vec::iterator j = i; j != res->end(); j++)
|
||||||
{
|
{
|
||||||
if (!*j)
|
if (!*j)
|
||||||
|
|
@ -604,22 +599,22 @@ namespace spot
|
||||||
else
|
else
|
||||||
delete tmpR;
|
delete tmpR;
|
||||||
|
|
||||||
if ((tmpGF != NULL) &&
|
if (tmpGF && tmpGF->size())
|
||||||
(tmpGF->size()))
|
|
||||||
{
|
{
|
||||||
ftmp = unop::instance(unop::G,
|
formula* ftmp
|
||||||
unop::instance(unop::F,
|
= unop::instance(unop::G,
|
||||||
multop::instance(mo->op(),
|
unop::instance(unop::F,
|
||||||
tmpGF)));
|
multop::instance(mo->op(),
|
||||||
|
tmpGF)));
|
||||||
tmpOther->push_back(ftmp);
|
tmpOther->push_back(ftmp);
|
||||||
}
|
}
|
||||||
if ((tmpFG != NULL) &&
|
if (tmpFG && tmpFG->size())
|
||||||
(tmpFG->size()))
|
|
||||||
{
|
{
|
||||||
ftmp = unop::instance(unop::F,
|
formula* ftmp
|
||||||
unop::instance(unop::G,
|
= unop::instance(unop::F,
|
||||||
multop::instance(mo->op(),
|
unop::instance(unop::G,
|
||||||
tmpFG)));
|
multop::instance(mo->op(),
|
||||||
|
tmpFG)));
|
||||||
tmpOther->push_back(ftmp);
|
tmpOther->push_back(ftmp);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -193,28 +193,24 @@ namespace spot
|
||||||
void
|
void
|
||||||
visit(multop* mo)
|
visit(multop* mo)
|
||||||
{
|
{
|
||||||
formula* f1 = NULL;
|
|
||||||
formula* f2 = NULL;
|
|
||||||
unsigned mos = mo->size();
|
unsigned mos = mo->size();
|
||||||
multop::vec* res = new multop::vec;
|
multop::vec* res = new multop::vec;
|
||||||
multop::vec::iterator index;
|
|
||||||
multop::vec::iterator indextmp;
|
|
||||||
|
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
for (unsigned i = 0; i < mos; ++i)
|
||||||
res->push_back(recurse(mo->nth(i)));
|
res->push_back(recurse(mo->nth(i)));
|
||||||
|
|
||||||
if (opt_ & Reduce_Syntactic_Implications)
|
if (opt_ & Reduce_Syntactic_Implications)
|
||||||
{
|
{
|
||||||
|
formula* f1;
|
||||||
|
formula* f2;
|
||||||
|
multop::vec::iterator index = res->begin();
|
||||||
|
multop::vec::iterator indextmp = index;
|
||||||
switch (mo->op())
|
switch (mo->op())
|
||||||
{
|
{
|
||||||
|
|
||||||
case multop::Or:
|
case multop::Or:
|
||||||
index = indextmp = res->begin();
|
|
||||||
if (index != res->end())
|
if (index != res->end())
|
||||||
{
|
break;
|
||||||
f1 = *index;
|
f1 = *index++;
|
||||||
index++;
|
|
||||||
}
|
|
||||||
for (; index != res->end(); index++)
|
for (; index != res->end(); index++)
|
||||||
{
|
{
|
||||||
f2 = *index;
|
f2 = *index;
|
||||||
|
|
@ -237,12 +233,9 @@ namespace spot
|
||||||
break;
|
break;
|
||||||
|
|
||||||
case multop::And:
|
case multop::And:
|
||||||
index = indextmp = res->begin();
|
if (index != res->end())
|
||||||
if (mos)
|
break;
|
||||||
{
|
f1 = *index++;
|
||||||
f1 = mo->nth(0);
|
|
||||||
index++;
|
|
||||||
}
|
|
||||||
for (; index != res->end(); index++)
|
for (; index != res->end(); index++)
|
||||||
{
|
{
|
||||||
f2 = *index;
|
f2 = *index;
|
||||||
|
|
|
||||||
|
|
@ -220,7 +220,6 @@ namespace spot
|
||||||
visit(const unop* uo)
|
visit(const unop* uo)
|
||||||
{
|
{
|
||||||
const formula* f1 = uo->child();
|
const formula* f1 = uo->child();
|
||||||
const formula* tmp = NULL;
|
|
||||||
switch (uo->op())
|
switch (uo->op())
|
||||||
{
|
{
|
||||||
case unop::Not:
|
case unop::Not:
|
||||||
|
|
@ -240,10 +239,8 @@ namespace spot
|
||||||
return;
|
return;
|
||||||
case unop::G:
|
case unop::G:
|
||||||
/* G(a) = false R a */
|
/* G(a) = false R a */
|
||||||
tmp = constant::false_instance();
|
if (syntactic_implication(f, constant::false_instance()))
|
||||||
if (syntactic_implication(f, tmp))
|
|
||||||
result_ = true;
|
result_ = true;
|
||||||
destroy(tmp);
|
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
/* Unreachable code. */
|
/* Unreachable code. */
|
||||||
|
|
|
||||||
|
|
@ -113,6 +113,9 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
|
||||||
grep -e 'return[ ]*[(][^(]*[)];' $tmp &&
|
grep -e 'return[ ]*[(][^(]*[)];' $tmp &&
|
||||||
diag 'No useless parentheses after delete.'
|
diag 'No useless parentheses after delete.'
|
||||||
|
|
||||||
|
grep 'NULL' $tmp &&
|
||||||
|
diag 'Use 0 instead of NULL. NULL is not portable.'
|
||||||
|
|
||||||
$fail && echo "$file" >>failures
|
$fail && echo "$file" >>failures
|
||||||
done
|
done
|
||||||
done
|
done
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue