#include <stdio.h>
#include <assert.h>

#include "cbmcLLRBContext.h"

void meta(struct Context*, enum Code);

/* cbmc built in functions */
int nondet_int() { return 9 ;}

// TODO c functions
void printTree(struct Node* node, int n) {
    if (node != 0) {
        printTree(node->left, n+1);
        for (int i=0;i<n;i++)
            printf("  ");
        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
        printTree(node->right, n+1);
    }
}


void verifySpecification(struct Context* context, struct Node* node) {
    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
        return meta(context, Exit);
    }
    printTree(context->data[Tree]->tree.root, 0);
    //assert(context->data[Tree]->tree.root->key == 0);

    int hoge      = nondet_int();
    node->key     = hoge;
    node->value   = node->key;
    context->next = VerifySpecification;
    context->loopCount++;

    return meta(context, Put);
}

void verifySpecification_stub(struct Context* context) {
    return verifySpecification(context, &context->data[Node]->node);
}


int main(int argc, char const* argv[]) {
    startCode(VerifySpecification);
    return 0;
}