alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

neverparse: accept more unparenthesised guards

Browse source 
Also accept guards of the form (a) || !(b) or (a) && !(b).

* src/neverparse/neverclaimscan.ll: Adjust.
* src/tgbatest/neverclaimread.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2013-07-26 12:02:04 +02:00
parent e598175fca
commit 027836f431
2 changed files with 4 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/neverparse/neverclaimscan.ll
View file

@ -75,7 +75,7 @@ eol \n|\r|\n\r|\r\n
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
} }
/* if we match ")&&(" or ")||(", stay in <in_par> mode */ /* if we match ")&&(" or ")||(", stay in <in_par> mode */
")"[ \t]*("&&"|"||")[ \t]*"(" { ")"[ \t]*("&&"|"||")[ \t!]*"(" {
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
} }
")" { ")" {

9
src/tgbatest/neverclaimread.test
View file

@ -117,7 +117,8 @@ cat >input <<EOF
never { /* p0 || p1 */ never { /* p0 || p1 */
accept_init: accept_init:
if if
:: (p1) || (p0) -> goto accept_all :: (p1) && (p0) -> goto accept_all
:: (p1) && !(p0) -> goto accept_all
fi; fi;
accept_all: accept_all:
skip skip
@ -130,20 +131,16 @@ digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
0 -> 1 0 -> 1
1 [label="accept_init", peripheries=2] 1 [label="accept_init", peripheries=2]
1 -> 2 [label="p1 | p0\n{Acc[1]}"] 1 -> 2 [label="p1\n{Acc[1]}"]
2 [label="accept_all", peripheries=2] 2 [label="accept_all", peripheries=2]
2 -> 2 [label="1\n{Acc[1]}"] 2 -> 2 [label="1\n{Acc[1]}"]
} }
EOF EOF
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed -e 's/p0 | p1/p1 | p0/g' stdout > tmp_ && mv tmp_ stdout
diff stdout expected diff stdout expected
rm input stdout expected rm input stdout expected
# Test broken guards in input # Test broken guards in input
cat >input <<EOF cat >input <<EOF
never { never {