# HG changeset patch
# User atton
# Date 1465284243 0
# Node ID c056a6a70c7e4260e0c243558cac517ded59c1a3
# Parent  be67b0312beaf6705fd8f2cf20ef58cc250f962c
WIP: insert verification using cbmc

diff -r be67b0312bea -r c056a6a70c7e .hgignore
--- a/.hgignore	Tue Jun 07 15:12:18 2016 +0900
+++ b/.hgignore	Tue Jun 07 07:24:03 2016 +0000
@@ -12,6 +12,9 @@
 cmake_install.cmake
 install_manifest.txt
 
+# cbmc
+cbmc_files
+
 # clang
 *.o
 *.bc
diff -r be67b0312bea -r c056a6a70c7e cbmc/insert_verification/insert_verification.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/insert_verification.sh	Tue Jun 07 07:24:03 2016 +0000
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+cd $(dirname $0)
+
+CBMC_FILE_DIR='cbmc_files'
+CBMC_INCLUDE_DIR="${CBMC_FILE_DIR}/include"
+LLRB_PATH=${GEARS_PATH}/src/llrb
+
+function copy_and_substitute() {
+    mkdir -p $2
+    filename="$2/$(basename $1)"
+    cp $1 $2
+    sed -i -e 's/goto/return/g' $filename
+    sed -i -e 's/__code/void/g' $filename
+}
+
+
+copy_and_substitute ${LLRB_PATH}/allocate.c ${CBMC_FILE_DIR}
+copy_and_substitute ${LLRB_PATH}/llrb.c     ${CBMC_FILE_DIR}
+copy_and_substitute ${LLRB_PATH}/compare.c  ${CBMC_FILE_DIR}
+copy_and_substitute ${LLRB_PATH}/stack.c    ${CBMC_FILE_DIR}
+
+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}
+
+
+#main.c
+#akashaCS.c
+#akashaLLRBContext.c
+#verifySpecification.c
+
+
+cbmc --unwind 50 -I ${CBMC_INCLUDE_DIR} cbmc_files/*.c main.c
diff -r be67b0312bea -r c056a6a70c7e cbmc/insert_verification/main.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/main.c	Tue Jun 07 07:24:03 2016 +0000
@@ -0,0 +1,12 @@
+#include <stdio.h>
+
+/* cbmc built in functions */
+int nondet_int();
+
+int main(int argc, char const* argv[]) {
+    for (int i = 0; i < 10; i++) {
+        put(nondet_int());
+        verifySpefication();
+    }
+    return 0;
+}