ltlcross: use tmpfile.
* src/bin/ltlcross.cc: Use features introduced by misc/tmpfile.hh.
This commit is contained in:
parent
c0e7f9de58
commit
9894b81775
1 changed files with 37 additions and 39 deletions
|
|
@ -56,6 +56,7 @@
|
||||||
#include "misc/escape.hh"
|
#include "misc/escape.hh"
|
||||||
#include "misc/hash.hh"
|
#include "misc/hash.hh"
|
||||||
#include "misc/random.hh"
|
#include "misc/random.hh"
|
||||||
|
#include "misc/tmpfile.hh"
|
||||||
|
|
||||||
// Disable handling of timeout on systems that miss kill() or alarm().
|
// Disable handling of timeout on systems that miss kill() or alarm().
|
||||||
// For instance MinGW.
|
// For instance MinGW.
|
||||||
|
|
@ -304,17 +305,6 @@ typedef std::vector<statistics_formula> statistics_vector;
|
||||||
statistics_vector vstats;
|
statistics_vector vstats;
|
||||||
std::vector<std::string> formulas;
|
std::vector<std::string> formulas;
|
||||||
|
|
||||||
// Cleanup temporary files.
|
|
||||||
std::list<std::string> toclean;
|
|
||||||
void
|
|
||||||
cleanup()
|
|
||||||
{
|
|
||||||
for (std::list<std::string>::const_iterator i = toclean.begin();
|
|
||||||
i != toclean.end(); ++i)
|
|
||||||
unlink(i->c_str());
|
|
||||||
toclean.clear();
|
|
||||||
}
|
|
||||||
|
|
||||||
static int
|
static int
|
||||||
to_int(const char* s)
|
to_int(const char* s)
|
||||||
{
|
{
|
||||||
|
|
@ -415,19 +405,6 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
static int
|
|
||||||
create_tmpfile(char c, unsigned int n, std::string& name)
|
|
||||||
{
|
|
||||||
char tmpname[30];
|
|
||||||
snprintf(tmpname, sizeof tmpname, "lck-%c%u-XXXXXX", c, n);
|
|
||||||
int fd = mkstemp(tmpname);
|
|
||||||
if (fd == -1)
|
|
||||||
error(2, errno, "failed to create a temporary file");
|
|
||||||
name = tmpname;
|
|
||||||
return fd;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
static volatile bool timed_out = false;
|
static volatile bool timed_out = false;
|
||||||
unsigned timeout_count = 0;
|
unsigned timeout_count = 0;
|
||||||
|
|
||||||
|
|
@ -463,7 +440,7 @@ sig_handler(int sig)
|
||||||
// forward signal
|
// forward signal
|
||||||
kill(-child_pid, sig);
|
kill(-child_pid, sig);
|
||||||
// cleanup files
|
// cleanup files
|
||||||
cleanup();
|
spot::cleanup_tmpfiles();
|
||||||
// and die verbosely
|
// and die verbosely
|
||||||
error(2, 0, "received signal %d", sig);
|
error(2, 0, "received signal %d", sig);
|
||||||
}
|
}
|
||||||
|
|
@ -539,19 +516,35 @@ namespace
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
struct printable_result_filename: public spot::printable_value<std::string>
|
struct printable_result_filename:
|
||||||
|
public spot::printable_value<spot::temporary_file*>
|
||||||
{
|
{
|
||||||
unsigned translator_num;
|
unsigned translator_num;
|
||||||
enum output_format { None, Spin, Lbtt };
|
enum output_format { None, Spin, Lbtt };
|
||||||
mutable output_format format;
|
mutable output_format format;
|
||||||
|
|
||||||
|
printable_result_filename()
|
||||||
|
{
|
||||||
|
val_ = 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
~printable_result_filename()
|
||||||
|
{
|
||||||
|
delete val_;
|
||||||
|
}
|
||||||
|
|
||||||
void reset(unsigned n)
|
void reset(unsigned n)
|
||||||
{
|
{
|
||||||
val_.clear();
|
|
||||||
translator_num = n;
|
translator_num = n;
|
||||||
format = None;
|
format = None;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void cleanup()
|
||||||
|
{
|
||||||
|
delete val_;
|
||||||
|
val_ = 0;
|
||||||
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
print(std::ostream& os, const char* pos) const
|
print(std::ostream& os, const char* pos) const
|
||||||
{
|
{
|
||||||
|
|
@ -559,11 +552,13 @@ namespace
|
||||||
format = Spin;
|
format = Spin;
|
||||||
else
|
else
|
||||||
format = Lbtt;
|
format = Lbtt;
|
||||||
if (!val_.empty())
|
if (val_)
|
||||||
error(2, 0, "you may have only one %%N or %%T specifier: %s",
|
error(2, 0, "you may have only one %%N or %%T specifier: %s",
|
||||||
translators[translator_num]);
|
translators[translator_num]);
|
||||||
close(create_tmpfile('o', translator_num,
|
char prefix[30];
|
||||||
const_cast<std::string&>(val_)));
|
snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
|
||||||
|
const_cast<printable_result_filename*>(this)->val_
|
||||||
|
= spot::create_tmpfile(prefix);
|
||||||
os << '\'' << val_ << '\'';
|
os << '\'' << val_ << '\'';
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
@ -628,14 +623,16 @@ namespace
|
||||||
void
|
void
|
||||||
string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
|
string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
|
||||||
{
|
{
|
||||||
int fd = create_tmpfile('i', n, tmpname);
|
char prefix[30];
|
||||||
|
snprintf(prefix, sizeof prefix, "lcr-i%u-", n);
|
||||||
|
spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix);
|
||||||
|
tmpname = tmpfile->name();
|
||||||
|
int fd = tmpfile->fd();
|
||||||
ssize_t s = str.size();
|
ssize_t s = str.size();
|
||||||
if (write(fd, str.c_str(), s) != s
|
if (write(fd, str.c_str(), s) != s
|
||||||
|| write(fd, "\n", 1) != 1)
|
|| write(fd, "\n", 1) != 1)
|
||||||
error(2, errno, "failed to write into %s", tmpname.c_str());
|
error(2, errno, "failed to write into %s", tmpname.c_str());
|
||||||
if (close(fd))
|
tmpfile->close();
|
||||||
error(2, errno, "failed to close %s", tmpname.c_str());
|
|
||||||
toclean.push_back(tmpname);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
const std::string&
|
const std::string&
|
||||||
|
|
@ -682,7 +679,6 @@ namespace
|
||||||
|
|
||||||
std::ostringstream command;
|
std::ostringstream command;
|
||||||
format(command, translators[translator_num]);
|
format(command, translators[translator_num]);
|
||||||
toclean.push_back(output.val());
|
|
||||||
|
|
||||||
assert(output.format != printable_result_filename::None);
|
assert(output.format != printable_result_filename::None);
|
||||||
|
|
||||||
|
|
@ -719,12 +715,13 @@ namespace
|
||||||
case printable_result_filename::Spin:
|
case printable_result_filename::Spin:
|
||||||
{
|
{
|
||||||
spot::neverclaim_parse_error_list pel;
|
spot::neverclaim_parse_error_list pel;
|
||||||
res = spot::neverclaim_parse(output, pel, &dict);
|
std::string filename = output.val()->name();
|
||||||
|
res = spot::neverclaim_parse(filename, pel, &dict);
|
||||||
if (!pel.empty())
|
if (!pel.empty())
|
||||||
{
|
{
|
||||||
std::ostream& err = global_error();
|
std::ostream& err = global_error();
|
||||||
err << "error: failed to parse the produced neverclaim.\n";
|
err << "error: failed to parse the produced neverclaim.\n";
|
||||||
spot::format_neverclaim_parse_errors(err, output, pel);
|
spot::format_neverclaim_parse_errors(err, filename, pel);
|
||||||
end_error();
|
end_error();
|
||||||
delete res;
|
delete res;
|
||||||
res = 0;
|
res = 0;
|
||||||
|
|
@ -734,7 +731,7 @@ namespace
|
||||||
case printable_result_filename::Lbtt:
|
case printable_result_filename::Lbtt:
|
||||||
{
|
{
|
||||||
std::string error;
|
std::string error;
|
||||||
std::ifstream f(output.val().c_str());
|
std::ifstream f(output.val()->name());
|
||||||
if (!f)
|
if (!f)
|
||||||
{
|
{
|
||||||
global_error() << "Cannot open " << output.val()
|
global_error() << "Cannot open " << output.val()
|
||||||
|
|
@ -794,6 +791,7 @@ namespace
|
||||||
double prec = XTIME_PRECISION;
|
double prec = XTIME_PRECISION;
|
||||||
st->time = (after - before) / prec;
|
st->time = (after - before) / prec;
|
||||||
}
|
}
|
||||||
|
output.cleanup();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
@ -1027,7 +1025,7 @@ namespace
|
||||||
nf->destroy();
|
nf->destroy();
|
||||||
}
|
}
|
||||||
|
|
||||||
cleanup();
|
spot::cleanup_tmpfiles();
|
||||||
++round;
|
++round;
|
||||||
|
|
||||||
if (!no_checks)
|
if (!no_checks)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue