fix unit tests

SRI-CSL · Aug 19, 2024 · 5baccd3 · 5baccd3
1 parent aacc130
commit 5baccd3
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 14 deletions.
diff --git a/tests/unit/test_dl_profiler.c b/tests/unit/test_dl_profiler.c
@@ -196,7 +196,7 @@ static int32_t test_dl_profiling(smt_benchmark_t *bench) {
     print_internalization_code(code);
   }
 
-  printf("term table: %"PRIu32" elements\n", context.terms->nelems);
+  printf("term table: %"PRIu32" elements\n", nterms(context.terms));
 
   profile = context.dl_profile;
   if (profile != NULL) {

diff --git a/tests/unit/test_int_queues.c b/tests/unit/test_int_queues.c
@@ -27,7 +27,7 @@ static void print_queue(int_queue_t *q) {
   uint32_t i;
 
   printf("queue %p\n", q);
-  printf("  size = %"PRIu32"\n", q->size);
+  printf("  size = %"PRIu32"\n", q->capacity);
   printf("  head = %"PRIu32"\n", q->head);
   printf("  tail = %"PRIu32"\n", q->tail);
   printf("  content:");
@@ -37,7 +37,7 @@ static void print_queue(int_queue_t *q) {
     }
     printf("\n");
   } else if (q->tail < q->head) {
-    for (i=q->head; i<q->size; i++) {
+    for (i=q->head; i<q->capacity; i++) {
       printf(" %"PRId32, q->data[i]);
     }
     for (i=0; i<q->tail; i++) {
@@ -53,7 +53,7 @@ static void print_queue_data(int_queue_t *q) {
   uint32_t i;
   printf("head = %"PRIu32", tail = %"PRIu32"\n", q->head, q->tail);
   printf("data:");
-  for (i=0; i<q->size; i++) printf(" %"PRId32, q->data[i]);
+  for (i=0; i<q->capacity; i++) printf(" %"PRId32, q->data[i]);
   printf("\n");
 }
 

diff --git a/tests/unit/test_pprod_table.c b/tests/unit/test_pprod_table.c
@@ -25,6 +25,7 @@
 #include <inttypes.h>
 
 #include "terms/pprod_table.h"
+#include "terms/terms.h"
 
 
 /*
@@ -77,25 +78,25 @@ static void print_pprod_table(FILE *f, pprod_table_t *table) {
   int32_t l;
 
   fprintf(f, "pprod_table %p\n", table);
-  fprintf(f, "  size = %"PRIu32"\n", table->size);
-  fprintf(f, "  nelems = %"PRIu32"\n", table->nelems);
-  fprintf(f, "  free_idx = %"PRId32"\n", table->free_idx);
+  fprintf(f, "  size = %"PRIu32"\n", table->pprods.size);
+  fprintf(f, "  nelems = %"PRIu32"\n", indexed_table_nelems(&table->pprods));
+  fprintf(f, "  free_idx = %"PRId32"\n", table->pprods.free_idx);
   fprintf(f, "  content:\n");
-  n = table->nelems;
+  n = indexed_table_nelems(&table->pprods);
   for (i=0; i<n; i++) {
-    p = table->data[i];
+    p = indexed_table_elem(pprod_table_elem_t, &table->pprods, i)->pprod;
     if (!has_int_tag(p)) {
       fprintf(f, "  data[%"PRIu32"] = ", i);
       print_varexp_array(f, p->prod, p->len);
       fprintf(f, "\n");
     }
   }
-  if (table->free_idx >= 0) {
+  if (table->pprods.free_idx >= 0) {
     fprintf(f, "  free list:");
-    l = table->free_idx;
+    l = table->pprods.free_idx;
     do {
       fprintf(f, " %"PRId32, l);
-      l = untag_i32(table->data[l]);
+      l = untag_i32(indexed_table_elem(pprod_table_elem_t, &table->pprods, l)->pprod);
     } while (l >= 0);
     fprintf(f, "\n");
   }

diff --git a/tests/unit/test_smt_blaster.c b/tests/unit/test_smt_blaster.c
@@ -373,7 +373,7 @@ int main(int argc, char *argv[]) {
   code = parse_smt_benchmark(&parser, &bench);
   if (code == 0) {
     printf("No syntax error found\n");
-    printf("term table: %"PRIu32" elements\n", __yices_globals.terms->nelems);
+    printf("term table: %"PRIu32" elements\n", nterms(__yices_globals.terms));
     fflush(stdout);
   } else {
     exit(YICES_EXIT_SYNTAX_ERROR);

diff --git a/tests/unit/test_smt_internalizer.c b/tests/unit/test_smt_internalizer.c
@@ -528,7 +528,7 @@ int main(int argc, char *argv[]) {
   code = parse_smt_benchmark(&parser, &bench);
   if (code == 0) {
     printf("No syntax error found\n");
-    printf("term table: %"PRIu32" elements\n", __yices_globals.terms->nelems);
+    printf("term table: %"PRIu32" elements\n", nterms(__yices_globals.terms));
   } else {
     exit(YICES_EXIT_SYNTAX_ERROR);
   }