ltlparse: diagnose empty (...) block in lenient mode.
* src/ltlparse/ltlparse.yy (try_recursive_parse): Diagnose empty strings. * src/ltltest/lenient.test: Add tests.
This commit is contained in:
parent
ff0eada81d
commit
676ab41f6f
2 changed files with 16 additions and 1 deletions
|
|
@ -108,6 +108,14 @@ using namespace spot::ltl;
|
|||
// Otherwise, we convert the string into an atomic proposition
|
||||
// (it's up to the environment to check the syntax of this
|
||||
// proposition, and maybe reject it).
|
||||
|
||||
if (str.empty())
|
||||
{
|
||||
error_list.push_back(parse_error(location,
|
||||
"unexpected empty block"));
|
||||
return 0;
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list suberror;
|
||||
const spot::ltl::formula* f;
|
||||
if (sere)
|
||||
|
|
@ -802,7 +810,7 @@ subformula: booleanatom
|
|||
delete $1;
|
||||
if (!$$)
|
||||
YYERROR;
|
||||
$$ = binop::instance(binop::EConcat, $$,
|
||||
$$ = binop::instance(binop::EConcat, $$,
|
||||
constant::true_instance());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -33,6 +33,7 @@ cat >input <<EOF
|
|||
(((a < b ) U ({( b == c - 1 )})))
|
||||
((((( a < b))) U ( b == c - 1)))
|
||||
((((( a < b))) U { b == c - 1}!))
|
||||
()a
|
||||
EOF
|
||||
|
||||
cat >expected <<EOF
|
||||
|
|
@ -44,7 +45,13 @@ cat >expected <<EOF
|
|||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
Xa
|
||||
EOF
|
||||
|
||||
run 0 $ltlfilt --lenient input > output
|
||||
cmp output expected
|
||||
|
||||
|
||||
|
||||
run 2 $ltlfilt --lenient -f 'F( )' 2> stderr
|
||||
grep 'unexpected empty block' stderr
|
||||
Loading…
Add table
Add a link
Reference in a new issue