# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1465279938 -32400
# Node ID be67b0312beaf6705fd8f2cf20ef58cc250f962c
# Parent  d2073e23f206be8015342aac8e75cc40fdce9070
Convert "showTrace" function to CodeSegment

diff -r d2073e23f206 -r be67b0312bea src/insert_verification/akashaLLRBContext.c
--- a/src/insert_verification/akashaLLRBContext.c	Tue Jun 07 14:39:07 2016 +0900
+++ b/src/insert_verification/akashaLLRBContext.c	Tue Jun 07 15:12:18 2016 +0900
@@ -6,6 +6,7 @@
 extern __code showTree_stub(struct Context*);
 extern __code iterateInsertion_stub(struct Context*);
 extern __code putAndGoToNextDepth_stub (struct Context*);
+extern __code showTrace_stub(struct Context*);
 extern __code verifySpecification_stub (struct Context*);
 extern __code duplicateIterator_stub(struct Context*);
 extern __code duplicateIteratorElem_stub(struct Context*);
@@ -69,7 +70,8 @@
     context->code[ShowTree]              = showTree_stub;
     context->code[IterateInsertion]      = iterateInsertion_stub;
     context->code[PutAndGoToNextDepth]   = putAndGoToNextDepth_stub;
-    context->code[VerifySpecification]   = verifySpecification_stub;;
+    context->code[ShowTrace]             = showTrace_stub;
+    context->code[VerifySpecification]   = verifySpecification_stub;
     context->code[DuplicateIterator]     = duplicateIterator_stub;
     context->code[DuplicateIteratorElem] = duplicateIteratorElem_stub;
     context->code[DuplicateTree]         = duplicateTree_stub;
diff -r d2073e23f206 -r be67b0312bea src/insert_verification/include/akashaLLRBContext.h
--- a/src/insert_verification/include/akashaLLRBContext.h	Tue Jun 07 14:39:07 2016 +0900
+++ b/src/insert_verification/include/akashaLLRBContext.h	Tue Jun 07 15:12:18 2016 +0900
@@ -8,6 +8,7 @@
     ShowTree,
     IterateInsertion,
     PutAndGoToNextDepth,
+    ShowTrace,
     VerifySpecification,
     DuplicateIterator,
     DuplicateIteratorElem,
diff -r d2073e23f206 -r be67b0312bea src/insert_verification/main.c
--- a/src/insert_verification/main.c	Tue Jun 07 14:39:07 2016 +0900
+++ b/src/insert_verification/main.c	Tue Jun 07 15:12:18 2016 +0900
@@ -96,6 +96,10 @@
     goto meta(context, Put);
 }
 
+__code showTrace_stub(struct Context* context) {
+    goto showTrace(context, &context->data[Iter]->iterator);
+}
+
 __code verifySpecification_stub(struct Context* context) {
     goto verifySpecification(context, &context->data[Tree]->tree, &context->data[Iter]->iterator);
 }
diff -r d2073e23f206 -r be67b0312bea src/insert_verification/verifySpecification.c
--- a/src/insert_verification/verifySpecification.c	Tue Jun 07 14:39:07 2016 +0900
+++ b/src/insert_verification/verifySpecification.c	Tue Jun 07 15:12:18 2016 +0900
@@ -1,16 +1,7 @@
-/* C functions (TODO: convert to code segment) */
-
 #include <stdio.h>
 #include "akashaLLRBContext.h"
 
-void showTrace(struct Iterator* iter) {
-    printf("show trace(reversed):");
-
-    for (; iter != NULL; iter = iter->previousDepth) {
-        printf("%u ", iter->iteratedValue);
-    }
-    printf("\n");
-}
+/* C functions (TODO: convert to code segment) */
 
 unsigned int min_height(struct Node* node, unsigned int height) {
     if ((node->left == NULL) && (node->right == NULL)) return height;
@@ -53,6 +44,17 @@
 
 /* Code Segments */
 
+__code showTrace(struct Context* context, struct Iterator* iter) {
+    printf("show trace(reversed):");
+
+    for (; iter != NULL; iter = iter->previousDepth) {
+        printf("%u ", iter->iteratedValue);
+    }
+    printf("\n");
+
+    goto meta(context, context->next);
+}
+
 __code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
     unsigned const int min_h = min_height(tree->root, 1);
     unsigned const int max_h = max_height(tree->root, 1);
@@ -61,8 +63,9 @@
         printf("llrb-condition violated.\n");
         printf("\tmin-height %u\n", min_h);
         printf("\tmax-height %u\n", max_h);
-        showTrace(iter);
-        exit(1);
+
+        context->next = Exit;
+        goto meta(context, ShowTrace);
     }
 
     goto meta(context, DuplicateIterator);