Commit Graph
8 Commits
Author SHA1 Message Date
Vincent ImbimboandAkim Demaille 2d8c3edbf8 cex: fix leaks
* src/state-item.c: Various functions were using heap allocated locals
and not freeing them.
2020-05-22 08:45:43 +02:00
Vincent ImbimboandAkim Demaille 482b370540 cex: fix stack overflow
* src/parse-simulation.c: Replace reference counting with
parse_state_retain everywhere.
(free_parse_state): Make this function iterative instead of
recursive. Long parse_state chains were causing stack exhaustion.

* tests/counterexample.at: Fix expectations.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille 66283fb625 cex: fix crash from zombie result
Fixes the SEGV in test 247 (counterexample.at:195): "S/R after first
token".

* src/counterexample.c: here.
* tests/counterexample.at: Fix expectations.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille dcb6c972a2 cex: add tests
* tests/counterexample.at: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille af0441cfd2 cex: bind counterexample generation
* src/complain.h, src/complain.c: Add support for -Wcounterexample.
* src/conflicts.c (report_counterexamples): New.
(rule_conflicts_print): Use it when -Wcounterexample is given.
* src/getargs.h, src/getargs.c: Add support for --trace=cex.
* src/main.c (main): Init and deinit counterexample generation.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille bbb63b1ca9 cex: introduce counterexample search
* src/counterexample.h, src/counterexample.c: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille ac54d19eba cex: introduce the parse simulator
* src/derivation.h, src/derivation.c,
* src/parse-simulation.h, src/parse-simulation.c: New.
2020-05-22 07:52:27 +02:00
Vincent ImbimboandAkim Demaille 5807dd9279 cex: add support for state-item pair graph generation
* src/lssi.h, src/lssi.c, src/state-item.h, src/state-item.c: New.
2020-05-22 07:52:27 +02:00