Commit Graph

55 Commits

Author SHA1 Message Date
Paul Eggert
b4582f1918 Update URLs to prefer https: to http:
Also, fix a few http: URLs that were no longer working.
2021-01-29 13:48:43 -08:00
Akim Demaille
d7e8aaa271 package: bump copyrights to 2021
Run 'make update-copyright'.
2021-01-16 16:11:17 +01:00
Akim Demaille
82133a6103 cex: add support for $TIME_LIMIT
* src/counterexample.c (TIME_LIMIT): Replace with...
(time_limit): this.
(counterexample_init): Check $TIME_LIMIT.
* src/scan-gram.l: Reorder includes.
2021-01-14 06:35:09 +01:00
Akim Demaille
3c36d871fa cex: display the rule numbers
From

    Example: "if" expr "then" "if" expr "then" stmt • "else" stmt
    Shift derivation
      if_stmt
      ↳ "if" expr "then" stmt
                         ↳ if_stmt
                           ↳ "if" expr "then" stmt • "else" stmt
    Reduce derivation
      if_stmt
      ↳ "if" expr "then" stmt                        "else" stmt
                         ↳ if_stmt
                           ↳ "if" expr "then" stmt •

to

    Example: "if" expr "then" "if" expr "then" stmt • "else" stmt
    Shift derivation
      if_stmt
      ↳ 3: "if" expr "then" stmt
                            ↳ 2: if_stmt
                                 ↳ 4: "if" expr "then" stmt • "else" stmt
    Example: "if" expr "then" "if" expr "then" stmt • "else" stmt
    Reduce derivation
      if_stmt
      ↳ 4: "if" expr "then" stmt                              "else" stmt
                            ↳ 2: if_stmt
                                 ↳ 3: "if" expr "then" stmt •

* src/state-item.h, src/state-item.c (state_item_rule): New.
* src/derivation.h, src/derivation.c (struct derivation): Add a rule
member.
Adjust dependencies.
* src/counterexample.c, src/parse-simulation.c: Pass the rule to
derivation_new.
* src/derivation.c (fprintf_if): New.
(derivation_width, derivation_print_tree_impl): Take the rule number
into account.

* tests/conflicts.at, tests/counterexample.at, tests/diagnostics.at,
* tests/report.at: Adjust.

* doc/bison.texi: Adjust.
2020-08-30 19:20:49 +02:00
Akim Demaille
12d0b15679 style: revert "avoid warnings with GCC 4.6"
This reverts commit d0bec3175f (which
should have read "We have a clash...", not "With have a clash...").
Now that `max()` was renamed `max_int()`, we can use `max` again, as
elsewhere in the code.

* src/counterexample.c (visited_hasher): Alpha reconversion.
2020-08-02 10:20:23 +02:00
Akim Demaille
977e19840d portability: beware of max () with MSVC
Reported by Maarten De Braekeleer.
https://lists.gnu.org/r/bison-patches/2020-07/msg00080.html

We don't want to use gnulib's min and max macros, since we use
function calls in min/max arguments.

* src/location.c (max_int, min_int): Move to...
* src/system.h: here.
* src/counterexample.c, src/derivation.c: Use max_int instead of max.
2020-08-02 08:19:35 +02:00
Akim Demaille
ece343d2c2 cex: style: prefer FOO_print to print_FOO
* src/state-item.h, src/state-item.c (print_state_item): Rename as...
(state_item_print): this.
* src/counterexample.c (print_counterexample): Rename as...
(counterexample_print): this.
2020-07-29 20:00:27 +02:00
Akim Demaille
d0bec3175f style: avoid warnings with GCC 4.6
With have a clash with the "max" function.

    src/counterexample.c: In function 'visited_hasher':
    src/counterexample.c:720:48: error: declaration of 'max' shadows a global declaration [-Werror=shadow]
    src/counterexample.c:116:12: error: shadowed declaration is here [-Werror=shadow]

* src/counterexample.c (visited_hasher): Alpha conversion.
2020-07-23 19:55:24 +02:00
Akim Demaille
b8c5e5609f cex: label all the derivations by their initial action
From

    input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
      Example: A b .
      First derivation
        a
        `-> A b .
      Second derivation
        a
        `-> A b
              `-> b .

to

    input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
      Example: A b .
      First reduce derivation
        a
        `-> A b .
      Second reduce derivation
        a
        `-> A b
              `-> b .

* src/counterexample.c (print_counterexample): here.
Compute the width of the labels to properly align the values.
* tests/conflicts.at, tests/counterexample.at, tests/diagnostics.at,
* tests/report.at: Adjust.
2020-07-20 07:36:38 +02:00
Akim Demaille
b81229e1f9 cex: improve readability of the subsections
Now that the derivation is no longer printed on one line, aligning the
example and the derivation is no longer useful.  It can actually be
harmful, as it makes the overall structure less clear.

* src/derivation.h, src/derivation.c (derivation_print_leaves): Remove
the `prefix` argument.
* src/counterexample.c (print_counterexample): Put the example next to
its label.
* tests/conflicts.at, tests/counterexample.at, tests/diagnostics.at,
* tests/report.at: Adjust.
2020-07-20 07:09:31 +02:00
Akim Demaille
815a76f558 cex: don't issue an empty line between counterexamples
Now that we use complain, the "sections" are clearer.

* src/counterexample.c (print_counterexample): Use the empty line only
in reports.
* tests/counterexample.at, tests/diagnostics.at, tests/report.at: Adjust.
2020-07-20 06:45:31 +02:00
Akim Demaille
ea138cd1f1 cex: use usual routines for diagnostics about S/R conflicts
See previous commit.  We go from

    input.y: warning: 3 reduce/reduce conflicts [-Wconflicts-rr]
    Shift/reduce conflict on token "⊕":
      Example              exp "+" exp • "⊕" exp
      Shift derivation
        exp
        ↳ exp "+" exp
                  ↳ exp • "⊕" exp

to

    input.y: warning: 3 reduce/reduce conflicts [-Wconflicts-rr]
    input.y: warning: shift/reduce conflict on token "⊕" [-Wcounterexamples]
      Example              exp "+" exp • "⊕" exp
      Shift derivation
        exp
        ↳ exp "+" exp
                  ↳ exp • "⊕" exp

with an hyperlink on -Wcounterexamples.

* src/counterexample.c (counterexample_report_shift_reduce):
Use complain.
* tests/counterexample.at, tests/diagnostics.at, tests/report.at:
Adjust.
2020-07-20 06:45:27 +02:00
Akim Demaille
9922f1f877 cex: use usual routines for diagnostics about R/R conflicts
This is more consistent, and brings benefits: users know that these
diagnostics are attached to -Wcounterexamples, and they can also click
on the hyperlink if permitted by their terminal.

We go from

    warning: 1 reduce/reduce conflict [-Wconflicts-rr]
    Reduce/reduce conflict on token $end:
      Example              A b .
      First derivation     a -> [ A b . ]
      Second derivation    a -> [ A b -> [ b . ] ]

to

    warning: 1 reduce/reduce conflict [-Wconflicts-rr]
    input.y: warning: reduce/reduce conflict on token $end [-Wcounterexamples]
      Example              A b .
      First derivation     a -> [ A b . ]
      Second derivation    a -> [ A b -> [ b . ] ]

with an hyperlink on -Wcounterexamples.

* src/counterexample.c (counterexample_report_reduce_reduce):
Use complain.
* tests/counterexample.at, tests/diagnostics.at, tests/report.at:
Adjust.
2020-07-20 06:45:21 +02:00
Akim Demaille
fff17fe8fe cex: display derivations as trees
Sometimes, understanding the derivations is difficult, because they
are serialized to fit in one line.  For instance, the example taken
from the NEWS file:

    %token ID
    %%
    s: a ID
    a: expr
    expr: expr ID ',' | "expr"

gave

    First example        expr • ID ',' ID $end
    Shift derivation     $accept → [ s → [ a → [ expr → [ expr • ID ',' ] ] ID ] $end ]
    Second example       expr • ID $end
    Reduce derivation    $accept → [ s → [ a → [ expr • ] ID ] $end ]

Printing as trees, it gives:

    First example        expr • ID ',' ID $end
    Shift derivation
      $accept
      ↳ s                      $end
        ↳ a                 ID
          ↳ expr
            ↳ expr • ID ','
    Second example       expr • ID $end
    Reduce derivation
      $accept
      ↳ s             $end
        ↳ a        ID
          ↳ expr •

* src/glyphs.h, src/glyphs.c (down_arrow, empty, derivation_separator):
New.
* src/derivation.c (derivation_print, derivation_print_impl): Rename
as...
(derivation_print_flat, derivation_print_flat_impl): These.
(fputs_if, derivation_depth, derivation_width, derivation_print_tree)
(derivation_print_tree_impl, derivation_print): New.
* src/counterexample.c (print_counterexample): Adjust.
* tests/conflicts.at, tests/counterexample.at, tests/diagnostics.at,
* tests/report.at: Adjust.
2020-07-18 07:54:02 +02:00
Akim Demaille
4d18195ebc cex: style changes
* src/counterexample.c: here.
2020-07-15 06:41:07 +02:00
Akim Demaille
4f9ae5de07 cex: display shifts before reductions
When reporting counterexamples for s/r conflicts, put the shift first.
This is more natural, and displays the default resolution first, which
is also what happens for r/r conflicts where the smallest rule number
is displayed first, and "wins".

* src/counterexample.c (counterexample): Add a shift_reduce member.
(new_counterexample): Adjust.
Swap the derivations when this is a s/r conflict.
(print_counterexample): For s/r conflicts, prefer "Shift derivation"
and "Reduce derivation" rather than "First/Second derivation".

* tests/conflicts.at, tests/counterexample.at, tests/report.at: Adjust.
* NEWS, doc/bison.texi: Ditto.
2020-07-14 06:48:48 +02:00
Akim Demaille
78f72a4516 style: s/lookahead_tokens/lookaheads/g
Currently we use both names.  Let's stick to the short one.

* src/AnnotationList.c, src/conflicts.c, src/counterexample.c,
* src/getargs.c, src/getargs.h, src/graphviz.c, src/ielr.c,
* src/lalr.c, src/print-graph.c, src/print-xml.c, src/print.c,
* src/state-item.c, src/state.c, src/state.h, src/tables.c:
s/lookahead_token/lookahead/gi.
2020-07-14 06:48:48 +02:00
Akim Demaille
c04693d651 cex: factor memory allocation
* src/counterexample.c (counterexample_report_state): Allocate once
per conflicted state, instead of once per r/r conflict.
2020-07-14 06:48:48 +02:00
Akim Demaille
12191911ba cex: use state_item_number consistently
* src/counterexample.c, src/state-item.c: here.
(counterexample_report_state): While at it, prefer c2 to j/k, to match
c1.
2020-07-14 06:48:48 +02:00
Akim Demaille
d7f27477f4 cex: more consistent memory allocation/copy
* src/counterexample.c, src/parse-simulation.c: It is more usual in
Bison to use sizeof on expressions than on types, especially for
allocation.
Let the compiler do it's job instead of calling memcpy ourselves.
2020-07-14 06:48:48 +02:00
Akim Demaille
5bad15d7ea cex: minor renaming
* src/counterexample.c (has_common_prefix): Rename as...
(have_common_prefix): this.
2020-07-14 06:48:48 +02:00
Akim Demaille
cd099edf2d cex: use better type names
There are too many gl_list_t in there, it's hard to understand what is
going on.  Introduce and use more precise types.  I sure can be wrong
in some places, it's hard to tell without proper tool support.

* src/counterexample.c, src/lssi.c, src/lssi.h, src/parse-simulation.c,
* src/parse-simulation.h, src/state-item.c, src/state-item.h
(si_bfs_node_list, search_state_list, ssb_list, lssi_list)
(state_item_list): New.
2020-07-14 06:48:48 +02:00
Akim Demaille
a2ad33dca6 style: cex: prefer the array notation
Prefer `&foos[i]` to `foos + i` when `foos` is an array.  IMHO, it
makes the semantics clearer.

* src/counterexample.c, src/lssi.c, src/parse-simulation.c,
* src/state-item.c: With arrays, prefer the array notation rather than
the pointer one.
2020-07-11 18:07:09 +02:00
Akim Demaille
5b2b7b1ffb style: cex: remove variables that don't make it simpler to read
* src/counterexample.c: With arrays, prefer the array notation rather
than the pointer one.
2020-07-11 18:07:09 +02:00
Akim Demaille
0895858d8e style: use 'nonterminal' consistently
* doc/bison.texi: Formatting changes.
* src/gram.h, src/gram.c (nvars): Rename as...
(nnterms): this.
Adjust dependencies.
(section): New.  Use it.
Replace "non terminal" and "non-terminal" by "nonterminal".
2020-06-27 11:39:32 +02:00
Akim Demaille
8f44164443 style: factor the access to a rule from its items
* src/counterexample.c (item_rule): Move to...
* src/counterexample.h: here.
* src/AnnotationList.c, src/counterexample.c, src/ielr.c: Use it.
2020-06-25 19:36:07 +02:00
Akim Demaille
b65bd16e45 cex: display all the S/R conflicts, not just one per (state, rule)
Before this commit, on

    %%
    exp
    : "if" exp "then" exp
    | "if" exp "then" exp "else" exp
    | exp "+" exp
    | "num"

we used to not display the third counterexample below:

    Shift/reduce conflict on token "+":
      Example              exp "+" exp . "+" exp
      First derivation     exp ::=[ exp ::=[ exp "+" exp . ] "+" exp ]
      Second derivation    exp ::=[ exp "+" exp ::=[ exp . "+" exp ] ]

    Shift/reduce conflict on token "else":
      Example              "if" exp "then" "if" exp "then" exp . "else" exp
      First derivation     exp ::=[ "if" exp "then" exp ::=[ "if" exp "then" exp . ] "else" exp ]
      Second derivation    exp ::=[ "if" exp "then" exp ::=[ "if" exp "then" exp . "else" exp ] ]

    Shift/reduce conflict on token "+":
      Example              "if" exp "then" exp . "+" exp
      First derivation     exp ::=[ exp ::=[ "if" exp "then" exp . ] "+" exp ]
      Second derivation    exp ::=[ "if" exp "then" exp ::=[ exp . "+" exp ] ]

    Shift/reduce conflict on token "+":
      Example              "if" exp "then" exp "else" exp . "+" exp
      First derivation     exp ::=[ exp ::=[ "if" exp "then" exp "else" exp . ] "+" exp ]
      Second derivation    exp ::=[ "if" exp "then" exp "else" exp ::=[ exp . "+" exp ] ]

* src/counterexample.c (counterexample_report_state): Don't stop of
the first conflicts.
* tests/conflicts.at, tests/counterexample.at, tests/diagnostics.at,
* tests/report.at: Adjust.
2020-06-23 06:56:04 +02:00
Akim Demaille
0f120354b6 cex: don't display twice unifying examples if there is no color
It makes no sense, and is actually confusing, to display twice the
same example with no visible difference.

* src/complain.h, src/complain.c (is_styled): New.
* src/counterexample.c (print_counterexample): Display the unified
example a second time only if it makes a difference.
* tests/conflicts.at, tests/counterexample.at, tests/report.at: Adjust.
* tests/diagnostics.at: Make sure we do display the unifying examples
twice when colors are enabled.  And check those colors.
2020-06-22 19:33:30 +02:00
Akim Demaille
9e75066819 cex: style changes
* src/counterexample.c: Simplify a bit.
* src/parse-simulation.c, src/parse-simulation.h: Enforce coding style.
2020-06-19 08:02:18 +02:00
Akim Demaille
d4f854e5b2 cex: also include the counterexamples in the report
The report is the best place to show the details about
counterexamples, since we have the state right under the nose.

For instance:

State 7

    1 exp: exp . "⊕" exp
    2    | exp . "+" exp
    2    | exp "+" exp .  [$end, "+", "⊕"]
    3    | exp . "+" exp
    3    | exp "+" exp .  [$end, "+", "⊕"]

    "⊕"  shift, and go to state 6

    $end      reduce using rule 2 (exp)
    $end      [reduce using rule 3 (exp)]
    "+"       reduce using rule 2 (exp)
    "+"       [reduce using rule 3 (exp)]
    "⊕"       [reduce using rule 2 (exp)]
    "⊕"       [reduce using rule 3 (exp)]
    $default  reduce using rule 2 (exp)

    Conflict between rule 2 and token "+" resolved as reduce (%left "+").

    Shift/reduce conflict on token "⊕":
        2 exp: exp "+" exp .
        1 exp: exp . "⊕" exp
      Example                  exp "+" exp • "⊕" exp
      First derivation         exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ]
      Example                  exp "+" exp • "⊕" exp
      Second derivation        exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ]

    Reduce/reduce conflict on tokens $end, "+", "⊕":
        2 exp: exp "+" exp .
        3 exp: exp "+" exp .
      Example                  exp "+" exp •
      First derivation         exp ::=[ exp "+" exp • ]
      Example                  exp "+" exp •
      Second derivation        exp ::=[ exp "+" exp • ]

    Shift/reduce conflict on token "⊕":
        3 exp: exp "+" exp .
        1 exp: exp . "⊕" exp
      Example                  exp "+" exp • "⊕" exp
      First derivation         exp ::=[ exp ::=[ exp "+" exp • ] "⊕" exp ]
      Example                  exp "+" exp • "⊕" exp
      Second derivation        exp ::=[ exp "+" exp ::=[ exp • "⊕" exp ] ]

* src/conflicts.h, src/conflicts.c (has_conflicts): New.
* src/counterexample.h, src/counterexample.c (print_counterexample):
Add a `prefix` argument.
(counterexample_report_shift_reduce)
(counterexample_report_reduce_reduce): Show the items when there's a
prefix.
* src/state-item.h, src/state-item.c (print_state_item):
Add a `prefix` argument.
* src/derivation.h, src/derivation.c (derivation_print)
(derivation_print_leaves): Add a prefix argument.
* src/print.c (print_state): When -Wcex is enabled, show the
conflicts.
* tests/report.at: Adjust.
2020-06-16 07:30:26 +02:00
Akim Demaille
35c0fe6789 cex: indent the diagnostics to highlight the structure
Instead of

    Shift/reduce conflict on token D:
    Example              A a • D
    First derivation     s ::=[ A a a ::=[ b ::=[ c ::=[ • ] ] ] d ::=[ D ] ]
    Example              A a • D
    Second derivation    s ::=[ A a d ::=[ • D ] ]

display

    Shift/reduce conflict on token D:
      Example              A a • D
      First derivation     s ::=[ A a a ::=[ b ::=[ c ::=[ • ] ] ] d ::=[ D ] ]
      Example              A a • D
      Second derivation    s ::=[ A a d ::=[ • D ] ]

* src/counterexample.c (print_counterexample): Indent.
* tests/counterexample.at: Adjust.
2020-06-16 07:29:46 +02:00
Akim Demaille
22f62414f9 cex: don't report the items
Showing the items (with the state numbers) is really something we
should restrict to the report.

* src/counterexample.c (counterexample_report_shift_reduce)
(counterexample_report_reduce_reduce): Don't show the pointed rules,
we will do that in the report.
* tests/counterexample.at: Adjust.
2020-06-16 07:29:46 +02:00
Akim Demaille
9206b15c4e cex: make sure traces go to stderr
* src/parse-simulation.h, src/parse-simulation.c (print_parse_state):
here.
2020-06-16 07:29:46 +02:00
Akim Demaille
5edac5e15a cex: add an argument to the reporting functions to specify the stream
* src/conflicts.c (find_state_item_number, report_state_counterexamples):
Move to...
* src/counterexample.h, src/counterexample.c (find_state_item_number)
(counterexample_report_state): this.
Add support for `out` as an argument.
(counterexample_report_reduce_reduce, counterexample_report_shift_reduce):
Accept an `out` argument, and be static.
2020-06-16 07:29:46 +02:00
Akim Demaille
d2acc4b401 cex: rename -Wcounterexample as -Wcounterexamples, and support -Wcex
Plural vs. singular is always a problem...

But we already have conflicts-sr and conflicts-rr, so counterexamples
makes more sense than counterexample.  Besides, -Wcounterexample will
still be accepted as an unambiguous prefix of -Wcounterexamples.

Add -Wcex as a convenient alias.

While at it, use only "counterexample", never "counter example".

* src/complain.h, src/complain.c
(Wcounterexample, warning_counterexample): Rename as...
(Wcounterexamples, warning_counterexamples): these.
(argmatch_warning_docs): Rename -Wcounterexample as -Wcounterexamples.
(argmatch_warning_args): Likewise.
Add support for -Wcex.
Adjust dependencies.
2020-06-10 07:53:44 +02:00
Akim Demaille
ae5edcc23b cex: color the counterexamples
Use colors to show the counterexamples and the derivations in color,
to highlight their structure.  Align the outputs, and add i18n
support. Reduce width by using a one-space separator instead of
two-space.

From

    Example  A  •  B  C
    First  derivation  s ::=[ a ::=[ A  • ]  x ::=[ B  C ] ]
    Second derivation  s ::=[ y ::=[ A  •  B ]  c ::=[ C ] ]

to

    Example              A • B C
    First derivation     s ::=[ a ::=[ A • ] x ::=[ B C ] ]
    Example              A • B C
    Second derivation    s ::=[ y ::=[ A • B ] c ::=[ C ] ]

with colors.

* data/bison-default.css (cex-dot, cex-0, cex-1, cex-2, cex-3, cex-4)
(cex-5, cex-6, cex-7, cex-step, cex-leaf): New.
* src/derivation.c (derivation_print_styled_impl): New.
(derivation_print, derivation_print_leaves): Use it.
* src/counterexample.c: Reformat the output.
* tests/counterexample.at: Adjust.
2020-06-07 09:18:58 +02:00
Akim Demaille
1ccb4be02b cex: reformat the s/r and r/r reports
In Bison we refer to "shift/reduce" conflicts, not "shift-reduce" (in
Bison 3.6.3 186 occurrences vs 15).  Enforce consistency on this.

Instead of "spending" a second line for each conflict to report the
lookaheads, put that on the same line as the type of conflict.  Also,
prefer "token" to "symbol".  Maybe we should even prefer "lookahead".
While at it, enable internationalization, with plurals where
appropriate.

As a consequence, instead of

    Shift-Reduce Conflict:
    6:    3 b: . %empty
    6:    6 d: c . A
    On Symbol: A

display

    Shift/reduce conflict on token A:
    6:    3 b: . %empty
    6:    6 d: c . A

* NEWS, doc/bison.texi, src/conflicts.c: Spell it "shift/reduce", not
"shift-reduce".
* src/counterexample.c (counterexample_report_shift_reduce)
(counterexample_report_reduce_reduce): Reformat and internationalize
output.
* tests/counterexample.at: Adjust expectations.
2020-06-07 09:18:58 +02:00
Akim Demaille
421662ec88 style: fix syntax-check issues
* src/counterexample.c, src/files.c, src/files.h, src/lssi.c,
* src/state-item.c: here.
2020-06-07 09:18:58 +02:00
Akim Demaille
ae03b16785 warnings: fix -Wmissing-prototypes issues
* src/counterexample.c, src/lssi.c, src/parse-simulation.c,
* src/state-item.c:
Here.
2020-06-03 08:31:08 +02:00
Akim Demaille
742910838e lists: fix various issues with the use of gnulib's list
First, we should avoid code such as

    gl_list_iterator_t it = gl_list_iterator (deriv->children);
    derivation *child = NULL;
    while (gl_list_iterator_next (&it, (const void **) &child, NULL))
      {
        derivation_print (child, f);

because of -Wstrict-aliasing (whose job is to catch type-punning
issues).  See https://lists.gnu.org/r/bug-bison/2020-05/msg00039.html.

Rather we need

    gl_list_iterator_t it = gl_list_iterator (deriv->children);
    const void **p = NULL;
    while (gl_list_iterator_next (&it, &p, NULL))
      {
        derivation *child = (derivation *) p;
        derivation_print (child, f);

Second, list iterators actually have destructors.  Even though they
are noop in the case of linked-lists, we should use them.

Let's address both issues with typed wrappers (such as
derivation_list_next) that take care of both issues, and besides allow
to scope the iterators within the loop:

    derivation *child;
    for (gl_list_iterator_t it = gl_list_iterator (deriv->children);
         derivation_list_next (&it, &child);
         )
      {
        derivation_print (child, f);

* src/derivation.h, src/derivation.c (derivation_list_next): New.
Use it where appropriate.
* src/counterexample.c (search_state_list_next): New.
Use it where appropriate.
* src/parse-simulation.h, src/parse-simulation.c
* src/state-item.h (state_item_list_next): New.
Use it where appropriate.
2020-06-01 18:50:35 +02:00
Akim Demaille
1ec93ca2a2 cex: clean the display of conflicted symbols
Instead of `On Symbols: {b,c,}`, display `On Symbols: b, c`.

* src/counterexample.c (counterexample_report_reduce_reduce): We don't
need braces.
Use commas as a separator, not a terminator.
* tests/counterexample.at: Adjust.
2020-05-23 18:23:07 +02:00
Vincent Imbimbo
99260caef9 cex: replace state-item data structures
* src/state-item.h: Add trans, prods, and revs edges to state-item
struct.
(si_trans, si_revs, si_prods_lookup): Remove.
* src/state-item.c, src/lssi.c, src/parse-simulation.c,
* src/counterexample.c: Update state-item API usage accordingly.
2020-05-22 08:45:44 +02:00
Vincent Imbimbo
c19af5cbb4 cex: fix bad reference counting
* src/counterexample.c (si_bfs_free): Fix reference_count
decrementing.
2020-05-22 08:45:44 +02:00
Vincent Imbimbo
b54181ff9b cex: fix miscellaneous leaks
* src/counterexample.c (unifying_counterexample): Always free
stage3result when it exists.
* src/conflicts.c (report_state_counterexamples): free leaked bitset.
* src/state-item.c (prune_disabled_paths): free leaked queue.
2020-05-22 08:45:44 +02:00
Vincent Imbimbo
86c45be582 cex: fix counterexample leak
* src/counterexample.c (free_counterexample): New.
Free counterexamples after printing.
2020-05-22 08:45:44 +02:00
Vincent Imbimbo
150b2318ed cex: fix parse state leaks
* src/parse_simulation.c: Fix bug in parse_state_free.
Free new_root when simulate_reduction generates zero states.

* src/parse-simulation.c, src/parse-simulation.h
(parse_state_list, parse_state_list_append): New.
* src/parse-simulation.c, src/parse-simulation.h,
* src/counterexample.c: Replace all uses of lists of parse states and
appends to parse_state_lists with the new API.
2020-05-22 08:45:44 +02:00
Vincent Imbimbo
35c4a8e65e cex: derivation reference counting
* src/derivation.h, src/derivation.c: Make derivation struct opaque.
Add derivation_list type for clarity.
(derivation_list_new): New.
(derivation_list_append): New.
(derivation_list_prepend): New.
(derivation_new_leaf): New constructor for derivations with no
children.
* src/counterexample.c, src/parse-simulation.c,
* src/parse-simulation.h: Replace uses of gl_list_t containing
derivations with derivation_list and its API.
Replace calls of dervation_new using null children with
derivation_new_leaf.
* src/parse-simulation.c: replace ps_chunk and its API with typed
versions si_chunk and deriv_chunk.
* src/parse-simlation.h, src/parse-simulation.c: Remove
parse_state_retain_deriv in favor of derivation reference counting.
* src/counterexample.c: Remove search_state_retain_deriv.
2020-05-22 08:45:44 +02:00
Akim Demaille
866bc6a49f cex: fix memory leaks when there are conflicts
* src/counterexample.c (production_step, reduction_step): Release
memory of temporary objects.
2020-05-22 08:45:43 +02:00
Akim Demaille
4590071287 style: use hash_xinsert
* gnulib: Update to get hash_xinsert.
Use it where appropriate.
2020-05-22 08:45:43 +02:00
Akim Demaille
f3ef847539 cex: stylistic changes
* src/counterexample.c: Use 'res' as a variable name for returned
value, as elsewhere.
Avoid uninitialized variables, especially pointers.
Avoid assignment where possible.
2020-05-22 08:45:43 +02:00