#!/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