Mercurial > hg > CbC > old > akasha

annotate src/insert_verification/verifySpecification.c @ 39:81717f43ea00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Convert C function to cs (getMaxHeight)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 13 Jun 2016 16:30:30 +0900
parents 593ab851ad76
children 56ea709e7af3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
31
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 #include <stdio.h>
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 #include "akashaLLRBContext.h"
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
4 extern void allocator(struct Context*);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
5
32
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
6 /* C functions (TODO: convert to code segment) */
31
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 unsigned int min_height(struct Node* node, unsigned int height) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 if ((node->left == NULL) && (node->right == NULL)) return height;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 if (node->left == NULL) return min_height(node->right, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 if (node->right == NULL) return min_height(node->left, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 unsigned int left_min = min_height(node->left, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 unsigned int right_min = min_height(node->right, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 if (left_min < right_min) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 return left_min;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 } else {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 return right_min;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 unsigned int max_height(struct Node* node, unsigned int height) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 if ((node->left == NULL) && (node->right == NULL)) return height;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 if (node->left == NULL) return max_height(node->right, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 if (node->right == NULL) return max_height(node->left, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 unsigned int left_max = max_height(node->left, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 unsigned int right_max = max_height(node->right, height+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 if (left_max > right_max) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 return left_max;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 } else {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 return right_max;
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 void printTree(struct Node* node, int n) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 if (node != 0) {
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 printTree(node->left, n+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 for (int i=0;i<n;i++)
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 printf(" ");
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 printTree(node->right, n+1);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 /* Code Segments */
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
32
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
49 __code showTrace(struct Context* context, struct Iterator* iter) {
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
50 printf("show trace(reversed):");
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
51
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
52 for (; iter != NULL; iter = iter->previousDepth) {
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
53 printf("%u ", iter->iteratedValue);
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
54 }
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
55 printf("\n");
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
56
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
57 goto meta(context, context->next);
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
58 }
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
59
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
60 __code getMinHeight_stub(struct Context* context) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
61 goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
62 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
63
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
64 __code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
65 const struct AkashaNode* akashaNode = akashaInfo->akashaNode;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
66
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
67 if (akashaNode == NULL) {
39
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
68 allocate->size = sizeof(struct AkashaNode);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
69 allocator(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
70 akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
71
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
72 akashaInfo->akashaNode->height = 1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
73 akashaInfo->akashaNode->node = context->data[Tree]->tree.root;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
74
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
75 goto getMaxHeight_stub(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
76 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
77
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
78 const struct Node* node = akashaInfo->akashaNode->node;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
79 if (node->left == NULL && node->right == NULL) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
80 if (akashaInfo->minHeight > akashaNode->height) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
81 akashaInfo->minHeight = akashaNode->height;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
82 akashaInfo->akashaNode = akashaNode->nextAkashaNode;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
83 goto getMinHeight_stub(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
84 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
85 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
86
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
87 akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
88
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
89 if (node->left != NULL) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
90 allocate->size = sizeof(struct AkashaNode);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
91 allocator(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
92 struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum];
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
93 left->height = akashaNode->height+1;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
94 left->node = node->left;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
95 left->nextAkashaNode = akashaInfo->akashaNode;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
96 akashaInfo->akashaNode = left;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
97 }
31
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
99 if (node->right != NULL) {
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
100 allocate->size = sizeof(struct AkashaNode);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
101 allocator(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
102 struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum];
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
103 right->height = akashaNode->height+1;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
104 right->node = node->right;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
105 right->nextAkashaNode = akashaInfo->akashaNode;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
106 akashaInfo->akashaNode = right;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
107 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
108
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
109 goto getMinHeight_stub(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
110 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
111
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
112 __code getMaxHeight_stub(struct Context* context) {
39
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
113 goto getMaxHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
114
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
115 }
39
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
116 __code getMaxHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
117 const struct AkashaNode* akashaNode = akashaInfo->akashaNode;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
118
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
119 if (akashaNode == NULL) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
120 allocate->size = sizeof(struct AkashaNode);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
121 allocator(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
122 akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
123
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
124 akashaInfo->akashaNode->height = 1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
125 akashaInfo->akashaNode->node = context->data[Tree]->tree.root;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
126
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
127 goto verifySpecificationFinish(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
128 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
129
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
130 /* FIXME: Reuse parts of getMinHeight */
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
131 const struct Node* node = akashaInfo->akashaNode->node;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
132 if (node->left == NULL && node->right == NULL) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
133 if (akashaInfo->maxHeight < akashaNode->height) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
134 akashaInfo->maxHeight = akashaNode->height;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
135 akashaInfo->akashaNode = akashaNode->nextAkashaNode;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
136 goto getMaxHeight_stub(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
137 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
138 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
139
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
140 akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
141
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
142 if (node->left != NULL) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
143 allocate->size = sizeof(struct AkashaNode);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
144 allocator(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
145 struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum];
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
146 left->height = akashaNode->height+1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
147 left->node = node->left;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
148 left->nextAkashaNode = akashaInfo->akashaNode;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
149 akashaInfo->akashaNode = left;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
150 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
151
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
152 if (node->right != NULL) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
153 allocate->size = sizeof(struct AkashaNode);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
154 allocator(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
155 struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum];
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
156 right->height = akashaNode->height+1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
157 right->node = node->right;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
158 right->nextAkashaNode = akashaInfo->akashaNode;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
159 akashaInfo->akashaNode = right;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
160 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
161
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
162 goto getMaxHeight_stub(context);
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
163 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
164
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
165 __code verifySpecification(struct Context* context, struct Allocate* allocate, struct Tree* tree, struct AkashaInfo* akashaInfo) {
39
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
166 if (tree->root == NULL) {
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
167 akashaInfo->minHeight = 1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
168 akashaInfo->maxHeight = 1;
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
169 goto verifySpecificationFinish(context);
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
170 }
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
171
38
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
172 akashaInfo->minHeight = -1;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
173 akashaInfo->maxHeight = 0;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
174
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
175 allocate->size = sizeof(struct AkashaNode);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
176 allocator(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
177 akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
178
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
179 akashaInfo->akashaNode->height = 1;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
180 akashaInfo->akashaNode->node = tree->root;
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
181
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
182 goto getMinHeight_stub(context);
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
183 }
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
184
593ab851ad76 Convert C function to cs (getMinHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
185 __code verifySpecificationFinish(struct Context* context) {
39
81717f43ea00 Convert C function to cs (getMaxHeight)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
186 if (context->data[AkashaInfo]->akashaInfo.minHeight > 2*context->data[AkashaInfo]->akashaInfo.maxHeight) {
32
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
187 context->next = Exit;
be67b0312bea Convert "showTrace" function to CodeSegment
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
188 goto meta(context, ShowTrace);
31
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 }
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 goto meta(context, DuplicateIterator);
d2073e23f206 Split verification functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 }