# HG changeset patch
# User atton
# Date 1465286393 0
# Node ID e06337c478c656a3b01820b870486e6e1b5c93d8
# Parent  30100c379f2f012e6f5b8a7cc7b9e39e4b77dd50
WIP: insert verification using cbmc

diff -r 30100c379f2f -r e06337c478c6 cbmc/insert_verification/insert_verification.sh
--- a/cbmc/insert_verification/insert_verification.sh	Tue Jun 07 07:29:31 2016 +0000
+++ b/cbmc/insert_verification/insert_verification.sh	Tue Jun 07 07:59:53 2016 +0000
@@ -22,7 +22,6 @@
 
 copy_and_substitute ${LLRB_PATH}/include/stack.h       ${CBMC_INCLUDE_DIR}
 
-copy_and_substitute ${LLRB_PATH}/include/llrbContext.h         ${CBMC_INCLUDE_DIR}
 copy_and_substitute ${GEARS_PATH}/src/include/origin_cs.h      ${CBMC_INCLUDE_DIR}
 
 
@@ -32,4 +31,4 @@
 #verifySpecification.c
 
 
-cbmc --unwind 50 -I ${CBMC_INCLUDE_DIR} cbmc_files/*.c main.c
+cbmc --unwind 50 -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
diff -r 30100c379f2f -r e06337c478c6 cbmc/insert_verification/main.c
--- a/cbmc/insert_verification/main.c	Tue Jun 07 07:29:31 2016 +0000
+++ b/cbmc/insert_verification/main.c	Tue Jun 07 07:59:53 2016 +0000
@@ -1,12 +1,29 @@
 #include <stdio.h>
 
+#include "cbmcLLRBContext.h"
+
 /* cbmc built in functions */
 int nondet_int();
 
-int main(int argc, char const* argv[]) {
+void verifySpecification_stub(struct Context* context) {
+    verifySpecification(context);
+}
+
+void verifySpecification(struct Context* context, struct Node* node) {
     for (int i = 0; i < 10; i++) {
-        put(nondet_int());
-        verifySpefication();
+        int hoge      = nodet_int();
+        node->key     = hoge;
+        node->value   = node->key;
+        context->next = VerifySpecification;
+
+        assert(&context->data[Tree]->tree.root->key == hoge);
+        meta(context, Put);
     }
+    meta(context, Exit);
+}
+
+
+int main(int argc, char const* argv[]) {
+    startCode(VerifySpecification);
     return 0;
 }