Do not store getenv() pointers in static variables.
... or the pointer might be invalidated if the environments changes. Fixes #63. * src/taalgos/dotty.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Copy the environment in strings instead. * wrap/python/tests/automata.ipynb: Adjust comment.
This commit is contained in:
parent
519f5e3cee
commit
125fa983ab
5 changed files with 71 additions and 31 deletions
|
|
@ -41,8 +41,18 @@ namespace spot
|
||||||
{
|
{
|
||||||
os_ << "digraph G {\n";
|
os_ << "digraph G {\n";
|
||||||
|
|
||||||
static const char* extra = getenv("SPOT_DOTEXTRA");
|
// Always copy the environment variable into a static string,
|
||||||
if (extra)
|
// so that we (1) look it up once, but (2) won't crash if the
|
||||||
|
// environment is changed.
|
||||||
|
static std::string extra = []()
|
||||||
|
{
|
||||||
|
auto s = getenv("SPOT_DOTEXTRA");
|
||||||
|
return s ? s : "";
|
||||||
|
}();
|
||||||
|
// Any extra text passed in the SPOT_DOTEXTRA environment
|
||||||
|
// variable should be output at the end of the "header", so
|
||||||
|
// that our setup can be overridden.
|
||||||
|
if (!extra.empty())
|
||||||
os_ << " " << extra << '\n';
|
os_ << " " << extra << '\n';
|
||||||
|
|
||||||
artificial_initial_state_ = t_automata_->get_artificial_initial_state();
|
artificial_initial_state_ = t_automata_->get_artificial_initial_state();
|
||||||
|
|
|
||||||
|
|
@ -88,13 +88,22 @@ namespace spot
|
||||||
{
|
{
|
||||||
case '.':
|
case '.':
|
||||||
{
|
{
|
||||||
static const char* def = getenv("SPOT_DOTDEFAULT");
|
// Copy the value in a string, so future calls to
|
||||||
|
// parse_opts do not fail if the environment has
|
||||||
|
// changed. (This matters particularly in an ipython
|
||||||
|
// notebook, where it is tempting to redefine
|
||||||
|
// SPOT_DOTDEFAULT.)
|
||||||
|
static std::string def = []()
|
||||||
|
{
|
||||||
|
auto s = getenv("SPOT_DOTDEFAULT");
|
||||||
|
return s ? s : "";
|
||||||
|
}();
|
||||||
// Prevent infinite recursions...
|
// Prevent infinite recursions...
|
||||||
if (orig == def)
|
if (orig == def.c_str())
|
||||||
throw std::runtime_error
|
throw std::runtime_error
|
||||||
(std::string("SPOT_DOTDEFAULT should not contain '.'"));
|
(std::string("SPOT_DOTDEFAULT should not contain '.'"));
|
||||||
if (def)
|
if (!def.empty())
|
||||||
parse_opts(def);
|
parse_opts(def.c_str());
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
case 'a':
|
case 'a':
|
||||||
|
|
@ -269,11 +278,18 @@ namespace spot
|
||||||
<< "\"\n node [fontname=\"" << opt_font_
|
<< "\"\n node [fontname=\"" << opt_font_
|
||||||
<< "\"]\n edge [fontname=\"" << opt_font_
|
<< "\"]\n edge [fontname=\"" << opt_font_
|
||||||
<< "\"]\n";
|
<< "\"]\n";
|
||||||
|
// Always copy the environment variable into a static string,
|
||||||
|
// so that we (1) look it up once, but (2) won't crash if the
|
||||||
|
// environment is changed.
|
||||||
|
static std::string extra = []()
|
||||||
|
{
|
||||||
|
auto s = getenv("SPOT_DOTEXTRA");
|
||||||
|
return s ? s : "";
|
||||||
|
}();
|
||||||
// Any extra text passed in the SPOT_DOTEXTRA environment
|
// Any extra text passed in the SPOT_DOTEXTRA environment
|
||||||
// variable should be output at the end of the "header", so
|
// variable should be output at the end of the "header", so
|
||||||
// that our setup can be overridden.
|
// that our setup can be overridden.
|
||||||
static const char* extra = getenv("SPOT_DOTEXTRA");
|
if (!extra.empty())
|
||||||
if (extra && *extra)
|
|
||||||
os_ << " " << extra << '\n';
|
os_ << " " << extra << '\n';
|
||||||
os_ << " I [label=\"\", style=invis, ";
|
os_ << " I [label=\"\", style=invis, ";
|
||||||
os_ << (opt_horizontal_ ? "width" : "height");
|
os_ << (opt_horizontal_ ? "width" : "height");
|
||||||
|
|
|
||||||
|
|
@ -766,8 +766,15 @@ namespace spot
|
||||||
if (!solution.second.empty())
|
if (!solution.second.empty())
|
||||||
res = sat_build(solution.second, d, a, state_based);
|
res = sat_build(solution.second, d, a, state_based);
|
||||||
|
|
||||||
static const char* log = getenv("SPOT_SATLOG");
|
// Always copy the environment variable into a static string,
|
||||||
if (log)
|
// so that we (1) look it up once, but (2) won't crash if the
|
||||||
|
// environment is changed.
|
||||||
|
static std::string log = []()
|
||||||
|
{
|
||||||
|
auto s = getenv("SPOT_SATLOG");
|
||||||
|
return s ? s : "";
|
||||||
|
}();
|
||||||
|
if (!log.empty())
|
||||||
{
|
{
|
||||||
std::fstream out(log,
|
std::fstream out(log,
|
||||||
std::ios_base::app | std::ios_base::out);
|
std::ios_base::app | std::ios_base::out);
|
||||||
|
|
@ -790,7 +797,7 @@ namespace spot
|
||||||
<< te.utime() << ',' << te.stime() << ','
|
<< te.utime() << ',' << te.stime() << ','
|
||||||
<< ts.utime() << ',' << ts.stime() << '\n';
|
<< ts.utime() << ',' << ts.stime() << '\n';
|
||||||
}
|
}
|
||||||
static const char* show = getenv("SPOT_SATSHOW");
|
static bool show = getenv("SPOT_SATSHOW");
|
||||||
if (show && res)
|
if (show && res)
|
||||||
dotty_reachable(std::cout, res);
|
dotty_reachable(std::cout, res);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -906,8 +906,15 @@ namespace spot
|
||||||
if (!solution.second.empty())
|
if (!solution.second.empty())
|
||||||
res = sat_build(solution.second, d, a, state_based);
|
res = sat_build(solution.second, d, a, state_based);
|
||||||
|
|
||||||
static const char* log = getenv("SPOT_SATLOG");
|
// Always copy the environment variable into a static string,
|
||||||
if (log)
|
// so that we (1) look it up once, but (2) won't crash if the
|
||||||
|
// environment is changed.
|
||||||
|
static std::string log = []()
|
||||||
|
{
|
||||||
|
auto s = getenv("SPOT_SATLOG");
|
||||||
|
return s ? s : "";
|
||||||
|
}();
|
||||||
|
if (!log.empty())
|
||||||
{
|
{
|
||||||
std::fstream out(log,
|
std::fstream out(log,
|
||||||
std::ios_base::app | std::ios_base::out);
|
std::ios_base::app | std::ios_base::out);
|
||||||
|
|
@ -930,7 +937,7 @@ namespace spot
|
||||||
<< te.utime() << ',' << te.stime() << ','
|
<< te.utime() << ',' << te.stime() << ','
|
||||||
<< ts.utime() << ',' << ts.stime() << '\n';
|
<< ts.utime() << ',' << ts.stime() << '\n';
|
||||||
}
|
}
|
||||||
static const char* show = getenv("SPOT_SATSHOW");
|
static bool show = getenv("SPOT_SATSHOW");
|
||||||
if (show && res)
|
if (show && res)
|
||||||
dotty_reachable(std::cout, res);
|
dotty_reachable(std::cout, res);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
{
|
{
|
||||||
"metadata": {
|
"metadata": {
|
||||||
"name": "",
|
"name": "",
|
||||||
"signature": "sha256:9b116e5c61ed241183bd5fb9cd5e35010cceb5043c2fab2be81473f829bc528e"
|
"signature": "sha256:c0ee6809405cd6426445a43cea6fc3448a99423e1a4be95efeda2fa03680f05f"
|
||||||
},
|
},
|
||||||
"nbformat": 3,
|
"nbformat": 3,
|
||||||
"nbformat_minor": 0,
|
"nbformat_minor": 0,
|
||||||
|
|
@ -13,10 +13,10 @@
|
||||||
"collapsed": false,
|
"collapsed": false,
|
||||||
"input": [
|
"input": [
|
||||||
"import os\n",
|
"import os\n",
|
||||||
"# Note that Spot (loaded by the kernel) will cache a \n",
|
"# Note that Spot (loaded by the kernel) will store a copy of\n",
|
||||||
"# pointer to the environment variable the first time it\n",
|
"# the environment variable the first time it reads them, so\n",
|
||||||
"# reads them. The Kernel may crash if you attempt to\n",
|
"# if you change those variables, the new values will be ignored\n",
|
||||||
"# modify the variables afterwards. See issue #63.\n",
|
"# until you restart the kernel.\n",
|
||||||
"os.environ['SPOT_DOTEXTRA'] = 'size=\"11,5\" node[style=filled,fillcolor=\"#ffffaa\"]'\n",
|
"os.environ['SPOT_DOTEXTRA'] = 'size=\"11,5\" node[style=filled,fillcolor=\"#ffffaa\"]'\n",
|
||||||
"os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
|
"os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
|
||||||
"import spot"
|
"import spot"
|
||||||
|
|
@ -159,7 +159,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc124150> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e8162150> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -291,7 +291,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f17fff640f0>"
|
"<IPython.core.display.SVG at 0x7fa0ead4a4e0>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -437,7 +437,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f17fc047f60>"
|
"<IPython.core.display.SVG at 0x7fa0e8083eb8>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -530,7 +530,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb930> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e8138930> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -600,7 +600,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fbb70> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e8138b70> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -669,7 +669,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb990> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e81389c0> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -785,7 +785,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f17ed8c7b38>"
|
"<IPython.core.display.SVG at 0x7fa0e803ab70>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -975,7 +975,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f17ed8c7a58>"
|
"<IPython.core.display.SVG at 0x7fa0e803ac88>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -1068,7 +1068,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fbb40> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e81389f0> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -1086,7 +1086,7 @@
|
||||||
{
|
{
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"output_type": "pyout",
|
"output_type": "pyout",
|
||||||
"prompt_number": 15,
|
"prompt_number": 13,
|
||||||
"svg": [
|
"svg": [
|
||||||
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
|
||||||
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
|
||||||
|
|
@ -1542,11 +1542,11 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7f17fc0fb9c0> >"
|
"<spot_impl.tgba_digraph; proxy of <Swig Object of type 'std::shared_ptr< spot::tgba_digraph > *' at 0x7fa0e8138b40> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 15
|
"prompt_number": 13
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"metadata": {}
|
"metadata": {}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue