Mercurial > hg > CbC > old > akasha
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