--- tests/counterexample.at | 357 ++++++++++++++++++++++++++++++++++++++++ tests/testsuite.at | 3 + 2 files changed, 360 insertions(+) create mode 100644 tests/counterexample.at
diff --git a/tests/counterexample.at b/tests/counterexample.at new file mode 100644 index 00000000..a42ea013 --- /dev/null +++ b/tests/counterexample.at @@ -0,0 +1,357 @@ +# Exercising Bison on conflicts. -*- Autotest -*- + +# Copyright (C) 2020 Free Software +# Foundation, Inc. + +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see <http://www.gnu.org/licenses/>. + +AT_BANNER([[Counterexamples.]]) + +## --------------------- ## +## Simple Unifying S/R. ## +## --------------------- ## + +AT_SETUP([Unifying S/R]) + +AT_DATA([[input.y]], +[[%token A B C +%% +s: a x | y c; +a: A; +c: C; +x: B | B C; +y: A | A B; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------- ## +## Deep Unifying S/R. ## +## ------------------- ## + +AT_SETUP([Deep Unifying S/R]) + +AT_DATA([[input.y]], +[[%token A B C +%% +s: ac | a bc; +ac: A ac C | b; +b: B | B b; +a: A | A a; +bc: B bc C | B C; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------------------------ ## +## S/R Conflict with Nullable Symbols. ## +## ------------------------------------ ## + +AT_SETUP([S/R Conflict with Nullable Symbols]) + +AT_DATA([[input.y]], +[[%token A B X Y +%% +s: ax by | A xby; +ax: A x; +x: %empty | X x; +by: B y; +y: %empty | Y y; +xby: B | X xby Y; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ---------------------------- ## +## Non-unifying Ambiguous S/R. ## +## ---------------------------- ## + +AT_SETUP([Non-unifying Ambiguous S/R]) + +AT_DATA([[input.y]], +[[%token A B C D E +%% +g: s | x; +s: A x E | A x D E; +x: b cd | bc; +b: B; +cd: C D; +bc: B C; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------------------ ## +## Non-unifying Unambiguous S/R. ## +## ------------------------------ ## + +AT_SETUP([Non-unifying Unambiguous S/R]) + +AT_DATA([[input.y]], +[[%token A B +%% +s: t | s t; +t: x | y; +x: A; +y: A A B; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ----------------------- ## +## S/R after first token. ## +## ----------------------- ## + +AT_SETUP([S/R after first token]) + +AT_DATA([[input.y]], +[[%token A B X Y +%% +a: r t | s; +r: b; +b: B; +t: A xx | A x xy; +s: b A xx y; +x: X; +xx: X X; +xy: X Y; +y: Y; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ----------------------------- ## +## Unifying R/R counterexample. ## +## ----------------------------- ## + +AT_SETUP([Unifying R/R counterexample]) + +AT_DATA([[input.y]], +[[%token A +%% +a : A b ; +b : A | b; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------------------- ## +## Non-unifying R/R lr1 conflict. ## +## ------------------------------- ## + +AT_SETUP([Non-unifying R/R lr1 conflict]) + +AT_DATA([[input.y]], +[[%token A B C D +%% +s: a A | B a C | b C | B b A; +a: D; +b: D; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------------------- ## +## Non-unifying R/R lr2 conflict. ## +## ------------------------------- ## + +AT_SETUP([Non-unifying R/R lr2 conflict]) + +AT_DATA([[input.y]], +[[%token H J K X +%% +s: a J; +a: H i; +i: X | i J K; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## -------------------- ## +## Cex Search Prepend. ## +## -------------------- ## + +# Tests prepend steps in uniying counterexample +# graph search + +AT_SETUP([Cex Search Prepend]) + +AT_DATA([[input.y]], +[[%token N A B C D +%% +s: n | n C; +n: N n D | N n C | N a B | N b; +a: A; +b: A B C | A B D; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------- ## +## R/R cex with prec. ## +## ------------------- ## + +# Tests that counterexamples containing rules using +# precedence/associativity directives work. + +AT_SETUP([R/R cex with prec]) + +AT_DATA([[input.y]], +[[%left b +%right c +%% +S: B C | C B; +A : B | C | %empty; +B : A b A; +C : A c A; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------- ## +## Null nonterminals. ## +## ------------------- ## + +AT_SETUP([Null nonterminals]) + +AT_DATA([[input.y]], +[[%token A +%% +a : b d | c d ; +b : ; +c : ; +d : a | c A | d; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## --------------------------- ## +## Non-unifying Prefix Share. ## +## --------------------------- ## + +AT_SETUP([Non-unifying Prefix Share]) + +# Tests for a counterexample which should start its derivation +# at a shared symbol rather than the start symbol. + +AT_DATA([[input.y]], +[[%token H J +%% +s: a | a J; +a: H i J J +i: %empty | i J; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## -------------------- ## +## Deep Null Unifying. ## +## ---------------------## + +# Tests that nested nullable nonterminals +# are derived correctly. + +AT_SETUP([Deep Null Unifying]) + +AT_DATA([[input.y]], +[[%token a d +%% +S: a A D | a A A D; +A: B; +B: C +C: %empty +D: d; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP + +## ------------------------ ## +## Deep Null Non-unifying. ## +## -------------------------## + +# Tests that expand_to_conflict works with nullable sybols + +AT_SETUP([Deep Null Non-unifying]) + +AT_DATA([[input.y]], +[[%token a d e +%% +S: a A D | a A A D e; +A: B; +B: C +C: %empty +D: d; +]]) + +AT_BISON_CHECK([-Wcounterexample input.y], 0, [], +[[ +]]) + +AT_CLEANUP \ No newline at end of file diff --git a/tests/testsuite.at b/tests/testsuite.at index 4ccbfd1e..f8d87639 100644 --- a/tests/testsuite.at +++ b/tests/testsuite.at @@ -44,6 +44,9 @@ m4_include([report.at]) # Conflicts detection and resolution. m4_include([conflicts.at]) +# Counterexaple generation. +m4_include([counterexample.at]) + # Support for #lines. m4_include([synclines.at]) -- 2.20.1 (Apple Git-117)
