diff --git a/src/Makefile.am b/src/Makefile.am
index 48cfc396d..4ba2cf2b8 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -50,7 +50,8 @@ libspot_la_LIBADD = \
ta/libta.la \
tgbaalgos/libtgbaalgos.la \
tgba/libtgba.la \
- tgbaparse/libtgbaparse.la
+ tgbaparse/libtgbaparse.la \
+ ../lib/libgnu.la
# Dummy C++ source to cause C++ linking.
nodist_EXTRA_libspot_la_SOURCES = _.cc
diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 45db2d663..cec99a3c1 100644
--- a/src/misc/Makefile.am
+++ b/src/misc/Makefile.am
@@ -20,7 +20,8 @@
## You should have received a copy of the GNU General Public License
## along with this program. If not, see .
-AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
+AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) \
+ -I$(top_builddir)/lib -I$(top_srcdir)/lib
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
miscdir = $(pkgincludedir)/misc
@@ -50,6 +51,7 @@ misc_HEADERS = \
position.hh \
random.hh \
timer.hh \
+ tmpfile.hh \
unique_ptr.hh \
version.hh
@@ -66,4 +68,5 @@ libmisc_la_SOURCES = \
optionmap.cc \
random.cc \
timer.cc \
+ tmpfile.cc \
version.cc
diff --git a/src/misc/tmpfile.cc b/src/misc/tmpfile.cc
new file mode 100644
index 000000000..daabe9916
--- /dev/null
+++ b/src/misc/tmpfile.cc
@@ -0,0 +1,128 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+
+#include "config.h"
+#include "tmpfile.hh"
+#include
+#include
+#include
+#include
+
+namespace spot
+{
+ namespace
+ {
+ std::list to_clean;
+
+ static
+ int create_temporary_file(const char* prefix,
+ const char* suffix,
+ char** name)
+ throw(std::bad_alloc, std::runtime_error)
+ {
+ size_t len = strlen(prefix);
+ size_t slen = 0;
+ if (suffix)
+ len += slen = strlen(suffix);
+ *name = static_cast(malloc(len + 6 + 1));
+ if (!name)
+ throw std::bad_alloc();
+ char* x = stpcpy(stpcpy(*name, prefix), "XXXXXX");
+ int fd;
+ if (suffix)
+ {
+ stpcpy(x, suffix);
+ fd = mkstemps(*name, slen);
+ }
+ else
+ {
+ fd = mkstemp(*name);
+ }
+ if (fd < 0)
+ throw std::runtime_error(std::string("failed to create ") + *name);
+ return fd;
+ }
+ }
+
+
+ temporary_file::temporary_file(char* name, cleanpos_t cp)
+ : name_(name), cleanpos_(cp)
+ {
+ }
+
+ temporary_file::~temporary_file()
+ {
+ unlink(name_);
+ free(name_);
+ to_clean.erase(cleanpos_);
+ }
+
+ open_temporary_file::open_temporary_file(char* name, cleanpos_t cp, int fd)
+ : temporary_file(name, cp), fd_(fd)
+ {
+ }
+
+ open_temporary_file::~open_temporary_file()
+ {
+ close();
+ }
+
+ void
+ open_temporary_file::close()
+ {
+ if (fd_ < 0)
+ return;
+ if (::close(fd_))
+ throw std::runtime_error(std::string("failed to close ") + name_);
+ fd_ = -1;
+ }
+
+ temporary_file*
+ create_tmpfile(const char* prefix, const char* suffix)
+ throw(std::bad_alloc, std::runtime_error)
+ {
+ char* name;
+ int fd = create_temporary_file(prefix, suffix, &name);
+ if (close(fd))
+ throw std::runtime_error(std::string("failed to close ") + name);
+ temporary_file::cleanpos_t cp = to_clean.insert(to_clean.end(), 0);
+ *cp = new temporary_file(name, cp);
+ return *cp;
+ }
+
+ open_temporary_file*
+ create_open_tmpfile(const char* prefix, const char* suffix)
+ throw(std::bad_alloc, std::runtime_error)
+ {
+ char* name;
+ int fd = create_temporary_file(prefix, suffix, &name);
+ open_temporary_file::cleanpos_t cp = to_clean.insert(to_clean.end(), 0);
+ open_temporary_file* otf = new open_temporary_file(name, cp, fd);
+ *cp = otf;
+ return otf;
+ }
+
+ void
+ cleanup_tmpfiles()
+ {
+ while (!to_clean.empty())
+ delete to_clean.front();
+ }
+}
+
diff --git a/src/misc/tmpfile.hh b/src/misc/tmpfile.hh
new file mode 100644
index 000000000..a170b0a4b
--- /dev/null
+++ b/src/misc/tmpfile.hh
@@ -0,0 +1,143 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+
+#ifndef SPOT_MISC_TMPFILE_HH
+# define SPOT_MISC_TMPFILE_HH
+
+# include "common.hh"
+# include
+# include
+# include
+# include
+# include "formater.hh"
+
+namespace spot
+{
+ /// \addtogroup misc_tools
+ /// @{
+
+ /// \brief Temporary file name
+ ///
+ /// This class serves a dual purpose.
+ ///
+ /// 1. It carries the name of a temporary file, created with
+ /// create_tmpfile().
+ /// 2. It represents the life of the associated file. The file is
+ /// erased as soon as the temporary_file instance is destroyed.
+ ///
+ /// Note that there are two ways to destroy temporary_file
+ /// instances. Either directly with delete, or indirectly by
+ /// calling cleanup_tmpfiles().
+ /// You should never delete an instance that has been created
+ /// before the last call to cleanup_tmpfiles(), because that
+ /// instance has already been deleted.
+ class SPOT_API temporary_file: public printable
+ {
+ public:
+ typedef std::list::iterator cleanpos_t;
+
+ SPOT_LOCAL temporary_file(char* name, cleanpos_t cp);
+ ~temporary_file();
+
+ const char* name() const
+ {
+ return name_;
+ }
+
+ friend std::ostream& operator<<(std::ostream& os, const temporary_file* f)
+ {
+ os << f->name();
+ return os;
+ }
+
+ virtual void
+ print(std::ostream& os, const char*) const
+ {
+ os << this;
+ }
+
+ protected:
+ char* name_;
+ cleanpos_t cleanpos_;
+ };
+
+ /// \brief Open temporary file
+ ///
+ /// This is a specialization of temporary_file that also holds an
+ /// open file descriptor, as created by create_open_tmpfile().
+ ///
+ /// Use the open_temporary_file::close() method if you want to close
+ /// that descriptor; do no call the POSIX close() function directly.
+ class SPOT_API open_temporary_file: public temporary_file
+ {
+ public:
+ SPOT_LOCAL open_temporary_file(char* name, cleanpos_t cp, int fd);
+ ~open_temporary_file();
+
+ void close();
+
+ int fd() const
+ {
+ return fd_;
+ }
+
+ protected:
+ int fd_;
+ };
+
+ /// \brief Create a temporary file.
+ ///
+ /// The file name will start with \a prefix, be followed by 6
+ /// randomish characters and will end in \a suffix. Usually suffix
+ /// is used to set an extension (you should include the dot).
+ ///
+ /// The temporary file is created and left empty. If you need
+ /// to fill it, consider using create_open_tmpfile() instead.
+ SPOT_API temporary_file*
+ create_tmpfile(const char* prefix, const char* suffix = 0)
+ throw(std::bad_alloc, std::runtime_error);
+
+ /// \brief Create a temporary file and leave it open for writing.
+ ///
+ /// Same as create_tmpfile, be leave the file open for writing. The
+ /// open_temporary_file::fd() method returns the file descriptor.
+ SPOT_API open_temporary_file*
+ create_open_tmpfile(const char* prefix, const char* suffix = 0)
+ throw(std::bad_alloc, std::runtime_error);
+
+ /// \brief Delete all temporary files.
+ ///
+ /// Delete all temporary files that have been created but haven't
+ /// been deleted so far. The verb "delete" should be understood as
+ /// both the C++ delete operator (all temporary_file and
+ /// open_temporary_file instance are destroyed) and as the file
+ /// system operation (the actual files are removed).
+ ///
+ /// Even in programs where temporary_file instance are consciously
+ /// destroyed when they are not needed, cleanup_tmpfiles() could
+ /// still be useful in signal handlers, for instance to clean all
+ /// temporary files upon SIGINT.
+ SPOT_API void
+ cleanup_tmpfiles();
+
+ /// @}
+}
+
+
+#endif // SPOT_MISC_TMPFILE_HH