view cbmc/insert_verification/insert_verification.sh @ 45:517d1108f91f

Tree height verification using cbmc
author atton
date Tue, 21 Jun 2016 01:07:31 +0000
parents e27f4961281e
children
line wrap: on
line source

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

rm -rf ${CBMC_FILE_DIR}

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}

cbmc --unwind 5 -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
#/bin/clang -Wall -O0 -g -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c