|
37
|
1 /* Context definition for llrb example */
|
|
|
2 #include "stack.h"
|
|
|
3
|
|
|
4 #define ALLOCATE_SIZE 20000000
|
|
|
5 #define LIMIT_OF_VERIFICATION_SIZE 5
|
|
|
6
|
|
|
7 enum Code {
|
|
|
8 /* for CBMC */
|
|
|
9 VerifySpecification,
|
|
|
10
|
|
|
11 /* definitions from llrb */
|
|
|
12 Allocator,
|
|
|
13 Put,
|
|
|
14 Replace,
|
|
|
15 Insert,
|
|
|
16 Compare,
|
|
|
17 RotateL,
|
|
|
18 RotateR,
|
|
|
19 SetTree,
|
|
|
20 InsertCase1,
|
|
|
21 InsertCase2,
|
|
|
22 InsertCase3,
|
|
|
23 InsertCase4,
|
|
|
24 InsertCase4_1,
|
|
|
25 InsertCase4_2,
|
|
|
26 InsertCase5,
|
|
|
27 StackClear,
|
|
|
28 Get,
|
|
|
29 Search,
|
|
|
30 Delete,
|
|
|
31 Delete1,
|
|
|
32 Delete2,
|
|
|
33 Delete3,
|
|
|
34 Replace_d1,
|
|
|
35 Replace_d2,
|
|
|
36 FindMax1,
|
|
|
37 FindMax2,
|
|
|
38 DeleteCase1,
|
|
|
39 DeleteCase2,
|
|
|
40 DeleteCase3,
|
|
|
41 DeleteCase4,
|
|
|
42 DeleteCase5,
|
|
|
43 DeleteCase6,
|
|
|
44 Exit,
|
|
|
45 };
|
|
|
46
|
|
|
47 enum Relational {
|
|
|
48 EQ,
|
|
|
49 GT,
|
|
|
50 LT,
|
|
|
51 };
|
|
|
52
|
|
|
53 enum UniqueData {
|
|
|
54 Allocate,
|
|
|
55 Tree,
|
|
|
56 Node,
|
|
|
57 };
|
|
|
58
|
|
|
59 struct Context {
|
|
|
60 enum Code next;
|
|
|
61 enum Code prev;
|
|
|
62 unsigned int codeNum;
|
|
|
63 void (**code) (struct Context*);
|
|
|
64 void* heapStart;
|
|
|
65 void* heap;
|
|
|
66 unsigned long heapLimit;
|
|
|
67 unsigned long dataNum;
|
|
|
68 stack_ptr code_stack;
|
|
|
69 stack_ptr node_stack;
|
|
|
70 union Data **data;
|
|
|
71
|
|
|
72 unsigned int loopCount;
|
|
|
73 };
|
|
|
74
|
|
|
75 union Data {
|
|
|
76 struct Comparable { // inteface
|
|
|
77 enum Code compare;
|
|
|
78 union Data* data;
|
|
|
79 } compare;
|
|
|
80 struct Count {
|
|
|
81 enum Code next;
|
|
|
82 long i;
|
|
|
83 } count;
|
|
|
84 struct Tree {
|
|
|
85 enum Code next;
|
|
|
86 struct Node* root;
|
|
|
87 struct Node* current;
|
|
|
88 struct Node* deleted;
|
|
|
89 int result;
|
|
|
90 } tree;
|
|
|
91 struct Node {
|
|
|
92 // need to tree
|
|
|
93 enum Code next;
|
|
|
94 int key; // comparable data segment
|
|
|
95 int value;
|
|
|
96 struct Node* left;
|
|
|
97 struct Node* right;
|
|
|
98 // need to balancing
|
|
|
99 enum Color {
|
|
|
100 Red,
|
|
|
101 Black,
|
|
|
102 } color;
|
|
|
103 } node;
|
|
|
104 struct Allocate {
|
|
|
105 enum Code next;
|
|
|
106 long size;
|
|
|
107 } allocate;
|
|
|
108 };
|
