Commit 2ceed595 authored by Marius Bozga's avatar Marius Bozga
Browse files

fix some C++ compilation warnings

parent b530e974
......@@ -64,6 +64,7 @@ int opt_limit_time = -1;
int opt_limit_states = -1;
int opt_limit_scn = -1;
int opt_limit_env = -1;
int opt_branch_min = 2;
/*
*
......@@ -306,12 +307,12 @@ void IfExplorator::alarm() {
m_time++;
status();
if(opt_limit_time > 0 && opt_limit_time <= m_time) {
if(0 < opt_limit_time && (unsigned) opt_limit_time <= m_time) {
fprintf(stderr, "\ntime limit reached\n");
fflush(stderr);
exit(10);
}
if(opt_limit_states > 0 && opt_limit_states <= q_count) {
if(0 < opt_limit_states && (unsigned) opt_limit_states <= q_count) {
fprintf(stderr, "\nstate limit reached\n");
fflush(stderr);
exit(11);
......@@ -432,8 +433,6 @@ void IfDfsExplorator::run() {
run(NULL);
}
int FIND_BRANCH_MIN=2;
void IfDfsExplorator::run(IfConfig* start) {
Successor* su = NULL;
Stack* st = NULL, *tt = NULL;
......@@ -480,7 +479,7 @@ void IfDfsExplorator::run(IfConfig* start) {
if (m_flags & PO) restrict();
if (m_flags & FB && length(dfs.stack->pending) >= FIND_BRANCH_MIN) {
if (m_flags & FB && length(dfs.stack->pending) >= (unsigned) opt_branch_min) {
dumpBranches();
m_flags &= ~FB;
}
......@@ -572,7 +571,7 @@ void IfDfsExplorator::restrictFeeds() {
dfs.stack->pending = NULL;
for(; su != NULL; su = st) {
st = su->next;
if (dfs.stack->feeds + su->label->count(IfEvent::FEED) <= opt_limit_env) {
if (dfs.stack->feeds + su->label->count(IfEvent::FEED) <= (unsigned) opt_limit_env) {
su->next = dfs.stack->pending;
dfs.stack->pending = su;
}
......@@ -629,7 +628,7 @@ void IfDfsExplorator::printStackRec(std::ostream &out, const Stack* left) const
}
void IfDfsExplorator::dumpBranches() const {
cout << "-- More than " << FIND_BRANCH_MIN << " dependent branches found in state. Scenario saved in fb.scn.\n";
cout << "-- More than " << opt_branch_min << " dependent branches found in state. Scenario saved in fb.scn.\n";
cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
for(Successor* fbs = dfs.stack->pending; fbs != NULL; fbs = fbs->next) {
cout << "-----------------------\n";
......@@ -1263,7 +1262,7 @@ int main(int argc, char* argv[]) {
}
}
else if (!strcmp(argv[i], "-fb")) {
FIND_BRANCH_MIN = (i == argc - 1) ? 2 : atoi(argv[i+1]);
opt_branch_min = (i == argc - 1) ? 2 : atoi(argv[i+1]);
flags |= IfExplorator::FB;
}
else if (!strcmp(argv[i], "-sp"))
......
Supports Markdown
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