datasheet-test: Check duplicate states before discarding them.
authorBen Pfaff <blp@gnu.org>
Sat, 30 May 2009 04:26:13 +0000 (21:26 -0700)
committerBen Pfaff <blp@gnu.org>
Sun, 7 Jun 2009 04:11:17 +0000 (21:11 -0700)
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

index 194f9223a00396801647f3372b4cd43d1ad0dce4..5eeb355346cf98fb82ee227d5925cf3a2f420a71 100644 (file)
@@ -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. */