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

neverparse: diagnose redefinition of state labels

Reported by Joachim Klein.

* src/neverparse/neverclaimparse.yy: Store labels and the
location of their first definition in a global map to catch
redefinitions.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention it.
parent 9a8becb8
......@@ -12,6 +12,8 @@ New in spot 1.2.5a (not yet released)
positive formula. The same procedure should be performed with
automata obtained from negated formulas, but because of a typo
this was not the case.
- the neverclaim parser will now diagnose redefinitions of
state labels.
New in spot 1.2.5 (2014-08-21)
......
......@@ -59,6 +59,7 @@
using namespace spot::ltl;
static bool accept_all_needed = false;
static bool accept_all_seen = false;
static std::map<std::string, spot::location> labels;
}
%token NEVER "never"
......@@ -77,7 +78,7 @@ static bool accept_all_seen = false;
%type <str> formula opt_dest
%type <p> transition src_dest
%type <list> transitions transition_block
%type <str> ident_list
%type <str> one_ident ident_list
%destructor { delete $$; } <str>
......@@ -108,12 +109,21 @@ states:
| states ';' state
| states ';'
ident_list:
IDENT ':'
one_ident: IDENT ':'
{
std::pair<std::map<std::string, spot::location>::const_iterator, bool>
res = labels.insert(std::make_pair(*$1, @1));
if (!res.second)
{
error(@1, std::string("redefinition of ") + *$1 + "...");
error(res.first->second, std::string("... ") + *$1 + " previously defined here");
}
$$ = $1;
}
| ident_list IDENT ':'
ident_list: one_ident
| ident_list one_ident
{
result->add_state_alias(*$2, *$1);
// Keep any identifier that starts with accept.
......@@ -294,6 +304,7 @@ namespace spot
}
accept_all_needed = false;
accept_all_seen = false;
labels.clear();
return result;
}
......
......@@ -169,7 +169,7 @@ run 2 ../ltl2tgba -XN input > stdout 2>stderr
cat >expected <<\EOF
input:9.16: syntax error, unexpected $undefined, expecting fi or ':'
EOF
grep input: stderr >> stderrfilt
grep input: stderr > stderrfilt
diff stderrfilt expected
......@@ -206,6 +206,87 @@ run 0 ../ltl2tgba -ks -XN input > output
diff output expected
# Test duplicated labels. The following neverclaim was produced by
# ltl2ba 1.1 for '[](<>[]p1 U X[]<>Xp0)', but is rejected by Spin
# because of a duplicate label (accept_S10). We should
# complain as well. This was reported by Joachim Klein.
cat >input <<\EOF
never { /* [](<>[]p1 U X[]<>Xp0) */
T0_init:
if
:: (1) -> goto accept_S2
:: (1) -> goto T1_S3
:: (p1) -> goto T2_S4
fi;
accept_S2:
if
:: (1) -> goto accept_S39
:: (1) -> goto T1_S24
:: (p1) -> goto accept_S10
fi;
accept_S39:
if
:: (p0) -> goto accept_S39
:: (1) -> goto T0_S39
:: (1) -> goto T0_S24
:: (p1) -> goto T0_S10
fi;
T0_S39:
if
:: (p0) -> goto accept_S39
:: (1) -> goto T0_S39
:: (1) -> goto T0_S24
:: (p1) -> goto T0_S10
fi;
T0_S24:
if
:: (1) -> goto T0_S24
:: (p1) -> goto T0_S10
fi;
T0_S10:
if
:: (p0 && p1) -> goto accept_S10
:: (p1) -> goto T0_S10
fi;
accept_S10:
if
:: (p0 && p1) -> goto accept_S10
:: (p1) -> goto T0_S10
fi;
T1_S24:
if
:: (1) -> goto T1_S24
:: (p1) -> goto accept_S10
fi;
accept_S10:
if
:: (p1) -> goto accept_S10
fi;
T1_S3:
if
:: (1) -> goto T1_S3
:: (1) -> goto T1_S24
:: (p1) -> goto T2_S4
:: (p1) -> goto accept_S10
fi;
T2_S4:
if
:: (p1) -> goto T2_S4
:: (p1) -> goto accept_S10
fi;
}
EOF
run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
cat stderr
cat >expected-err <<\EOF
input:48.1-10: redefinition of accept_S10...
input:38.1-10: ... accept_S10 previously defined here
EOF
grep input: stderr > stderrfilt
diff stderrfilt expected-err
cat >formulae<<EOF
a
FG a
......
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