[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PATCH] cex: fix crash from zombie result
From: |
Vincent Imbimbo |
Subject: |
[PATCH] cex: fix crash from zombie result |
Date: |
Sat, 16 May 2020 11:32:29 -0400 |
---
src/counterexample.c | 18 ++++++++++++++----
1 file changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/counterexample.c b/src/counterexample.c
index bcfc6fa6..dffca1f8 100644
--- a/src/counterexample.c
+++ b/src/counterexample.c
@@ -567,6 +567,13 @@ search_state_free (search_state *ss)
free (ss);
}
+static inline void
+search_state_retain_derivs (search_state *ss)
+{
+ parse_state_retain_deriv (ss->states[0]);
+ parse_state_retain_deriv (ss->states[1]);
+}
+
static void
search_state_print (search_state *ss)
{
@@ -1070,12 +1077,11 @@ unifying_example (state_item_number itm1,
// we've found a unifying counterexample.
cex = new_counterexample (d1, d2, true, false);
// prevent d1/d2 from being freed.
- parse_state_retain_deriv (ps1);
- parse_state_retain_deriv (ps2);
+ search_state_retain_derivs (ss);
goto cex_search_end;
}
if (!stage3result)
- stage3result = ss;
+ stage3result = copy_search_state (ss);
}
}
if (TIME_LIMIT_ENFORCED)
@@ -1107,7 +1113,11 @@ cex_search_end:;
// If a search state from Stage 3 is available, use it
// to construct a more compact nonunifying counterexample.
if (stage3result)
- cex = complete_diverging_examples (stage3result, next_sym);
+ {
+ cex = complete_diverging_examples (stage3result, next_sym);
+ search_state_retain_derivs (stage3result);
+ search_state_free (stage3result);
+ }
// Otherwise, construct a nonunifying counterexample that
// begins from the start state using the shortest
// lookahead-sensitive path to the reduce item.
--
2.20.1 (Apple Git-117)
- [PATCH] cex: fix crash from zombie result,
Vincent Imbimbo <=