Mercurial > hg > CbC > old > akasha

comparison cbmc/insert_verification/include/cbmcLLRBContext.h @ 37:e27f4961281e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP: insert verification using cbmc (syntax valid)
author atton
date Mon, 13 Jun 2016 01:35:37 +0000
parents
children 517d1108f91f
comparison
equal deleted inserted replaced
36:9619480d0dc0 37:e27f4961281e
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 };