Commit 9e7d0677 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

parseaut: better diagnostic of unsupported versions

* src/parseaut/parseaut.yy: Add and the a check_version() function.
* src/tests/parseaut.test: Test it.
* NEWS: Mention it.
parent 0671d628
......@@ -36,6 +36,9 @@ New in spot 1.99.4a (not yet released)
the language, but it speedup some algorithms like NDFS-based
emptiness checks, as discussed in our Spin'15 paper.)
* The HOA parser will diagnose any version that is not v1, unless it
looks like a subversion of v1 and no parse error was detected.
Python:
* Add bindings for complete() and dtwa_complement()
......
......@@ -29,6 +29,8 @@
%code requires
{
#include "config.h"
#include "misc/common.hh"
#include <string>
#include <cstring>
#include <sstream>
......@@ -39,6 +41,11 @@
#include "priv/accmap.hh"
#include "tl/parse.hh"
#ifndef HAVE_STRVERSCMP
// If the libc does not have this, a version is compiled in lib/.
extern "C" int strverscmp(const char *s1, const char *s2);
#endif
inline namespace hoayy_support
{
typedef std::map<int, bdd> map_t;
......@@ -71,6 +78,8 @@
spot::location used_loc;
};
spot::parsed_aut_ptr h;
std::string format_version;
spot::location format_version_loc;
spot::environment* env;
formula_cache fcache;
named_tgba_t* namer = nullptr;
......@@ -418,8 +427,8 @@ header: format-version header-items
version: IDENTIFIER
{
if (*$1 != "v1")
error(@$, "unsupported version of the HOA format");
res.format_version = *$1;
res.format_version_loc = @1;
delete $1;
}
......@@ -1435,7 +1444,7 @@ nc-formula: nc-formula-or-ident
nc-opt-dest:
/* empty */
{
$$ = 0;
$$ = nullptr;
}
| "->" "goto" IDENTIFIER
{
......@@ -1457,7 +1466,7 @@ nc-src-dest: nc-formula nc-opt-dest
// fi
if (!$2)
{
$$ = 0;
$$ = nullptr;
}
else
{
......@@ -1847,6 +1856,37 @@ static void fix_properties(result_& r)
r.h->aut->prop_state_based_acc();
}
static void check_version(const result_& r,
spot::parse_aut_error_list& error_list)
{
if (r.h->type != spot::parsed_aut_type::HOA)
return;
auto& v = r.format_version;
if (v.size() < 2 || v[0] != 'v' || v[1] < '1' || v[1] > '9')
{
error_list.emplace_front(r.format_version_loc, "unknown HOA version");
return;
}
const char* beg = &v[1];
char* end = nullptr;
long int vers = strtol(beg, &end, 10);
if (vers != 1)
{
error_list.emplace_front(r.format_version_loc, "unsupported HOA version");
return;
}
constexpr const char supported[] = "1";
if (strverscmp(supported, beg) < 0 && !error_list.empty())
{
std::ostringstream s;
s << "we can read HOA v" << supported
<< " but this file uses " << v << "; this might "
<< "cause the following errors";
error_list.emplace_front(r.format_version_loc, s.str());
return;
}
}
namespace spot
{
automaton_stream_parser::automaton_stream_parser(const std::string& name,
......@@ -1906,6 +1946,7 @@ namespace spot
// Bison 3.0.2 lacks a += operator for locations.
r.h->loc = r.h->loc + e.pos;
}
check_version(r, error_list);
last_loc = r.h->loc;
last_loc.step();
if (r.h->aborted)
......
......@@ -250,17 +250,28 @@ State: 1 {0}
HOA: v2
--BODY--
--END--
HOA: w1
--BODY--
--END--
HOA: v1_1
--BODY--
--END--
EOF
t='this might cause the following errors'
expecterr input <<EOF
input:5.19: number is larger than the count of acceptance sets...
input:5.1-13: ... declared here.
input:12.6-7: unsupported version of the HOA format
input:12.6-7: unsupported HOA version
input:12.1-7: missing 'Acceptance:' header
input:15.6-7: unknown HOA version
input:15.1-7: missing 'Acceptance:' header
input:18.6-9: we can read HOA v1 but this file uses v1_1; $t
input:18.1-9: missing 'Acceptance:' header
EOF
cat >input<<EOF
HOA: v1
HOA: v1a /* version greater than 1, but assumed to be compatible */
States: 3
Start: 0
acc-name: generalized-Buchi 2
......
Markdown is supported
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