From 6171d2d41a551af903fd444e10f77bb77b563359 Mon Sep 17 00:00:00 2001 From: Ben Pfaff Date: Fri, 29 May 2009 21:26:13 -0700 Subject: [PATCH] datasheet-test: Check duplicate states before discarding them. By failing to check states whose hashes already appeared in the model checker table, the datasheet test was missing some bugs. This commit changes the datasheet test code to check the state before it checks for the hash. --- tests/data/datasheet-test.c | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/tests/data/datasheet-test.c b/tests/data/datasheet-test.c index 194f9223..5eeb3553 100644 --- a/tests/data/datasheet-test.c +++ b/tests/data/datasheet-test.c @@ -188,14 +188,6 @@ check_datasheet (struct mc *mc, struct datasheet *ds, assert (n_rows < MAX_ROWS); assert (n_columns < MAX_COLS); - /* If it is a duplicate hash, discard the state before checking - its consistency, to save time. */ - if (mc_discard_dup_state (mc, hash_datasheet (ds))) - { - datasheet_destroy (ds); - return; - } - /* Check contents of datasheet via datasheet functions. */ if (!check_caseproto (mc, proto, datasheet_get_proto (ds), "datasheet")) { @@ -316,7 +308,10 @@ check_datasheet (struct mc *mc, struct datasheet *ds, "have been (size %zu,%zu)", n_rows, n_columns); } - mc_add_state (mc, ds); + if (mc_discard_dup_state (mc, hash_datasheet (ds))) + datasheet_destroy (ds); + else + mc_add_state (mc, ds); } /* Extracts the contents of DS into DATA. */ -- 2.30.2