/* Context definition for llrb example */
#include "stack.h"

#define ALLOCATE_SIZE 20000000
#define LIMIT_OF_VERIFICATION_SIZE 5

enum Code {
    /* for CBMC */
    VerifySpecification,

    /* definitions from llrb */
    Allocator,
    Put,
    Replace,
    Insert,
    Compare,
    RotateL,
    RotateR,
    SetTree,
    InsertCase1,
    InsertCase2,
    InsertCase3,
    InsertCase4,
    InsertCase4_1,
    InsertCase4_2,
    InsertCase5,
    StackClear,
    Get,
    Search,
    Delete,
    Delete1,
    Delete2,
    Delete3,
    Replace_d1,
    Replace_d2,
    FindMax1,
    FindMax2,
    DeleteCase1,
    DeleteCase2,
    DeleteCase3,
    DeleteCase4,
    DeleteCase5,
    DeleteCase6,
    Exit,
};

enum Relational {
    EQ,
    GT,
    LT,
};

enum UniqueData {
    Allocate,
    Tree,
    Node,
};

struct Context {
    enum Code next;
    enum Code prev;
    unsigned int codeNum;
    void (**code) (struct Context*);
    void* heapStart;
    void* heap;
    unsigned long heapLimit;
    unsigned long dataNum;
    stack_ptr code_stack;
    stack_ptr node_stack;
    union Data **data;

    unsigned int loopCount;
};

union Data {
    struct Comparable { // inteface
        enum Code compare;
        union Data* data;
    } compare;
    struct Count {
        enum Code next;
        long i;
    } count;
    struct Tree {
        enum Code next;
        struct Node* root;
        struct Node* current;
        struct Node* deleted;
        int result;
    } tree;
    struct Node {
        // need to tree
        enum Code next;
        int key; // comparable data segment
        int value;
        struct Node* left;
        struct Node* right;
        // need to balancing
        enum Color {
            Red,
            Black,
        } color;
    } node;
    struct Allocate {
        enum Code next;
        long size;
    } allocate;
};