1#! /bin/bash 2# 3# I normaly use /bin/sh, but that is broken on our SUNs.... 4# 5# Usage: cd E;spec_version.sh <dest> 6# 7# - Copy all public core source files for eprover to <dest> 8# - Remove all __inline__ stuff 9# - Transform all CLIB includes to "" form 10# - Create Makefile.flat 11# - Add "#define NDEBUG" to clb_defines.h" 12# - Add other SPEC-specific defines 13 14if [ "$1" = "" ] ; then 15 echo "spec_version: Usage: spec_version.sh <dest>" 16 exit 1 17fi; 18 19if test -e $1 ; then 20 echo "spec_version: Target directory $1 exists" 21 exit 1; 22fi; 23 24mkdir $1 25cp [^Si]*/*.[ch] $1 26cp etc/Makefile.flat.template1 $1/Makefile.flat 27cp etc/Makefile.flat.template2 $1/Makefile.tmp 28cd $1 29touch CSSCPA_filter.c cex_csscpa.c cex_csscpa.h che_G_E___auto.c \ 30 che_G_N___auto.c che_H_____auto.c che_U_____auto.c \ 31 checkproof.c classify_problem.c direct_examples.c eground.c \ 32 ekb_create.c ekb_delete.c ekb_ginsert.c ekb_insert.c \ 33 epclanalyse.c epclextract.c patterntest.c \ 34 proofanalyze.c termprops.c tsm_classify.c clb_newmem.[ch] \ 35 cl_test.c edpll.c csl_bla epcllemma.c 36rm CSSCPA_filter.c cex_csscpa.c cex_csscpa.h che_G_E___auto.c \ 37 che_G_N___auto.c che_H_____auto.c che_U_____auto.c \ 38 checkproof.c classify_problem.c direct_examples.c eground.c \ 39 ekb_create.c ekb_delete.c ekb_ginsert.c ekb_insert.c \ 40 epclanalyse.c epclextract.c patterntest.c \ 41 proofanalyze.c termprops.c tsm_classify.c clb_newmem.[ch] \ 42 cl_test.c edpll.c csl* epcllemma.c 43 44for file in *.[ch] ; do 45 gawk '/#include *<..._.*>/{gsub(/[<>]/,"\""); print; next}{print}' $file | sed -e 's/__inline__//' |sed -e 's/# Failure:/# No proof found:/' > tmpfile 46 mv tmpfile $file 47done; 48 49 50echo "PROJ="`ls *.c | grep -v che_X_____auto | grep -v che_auto_cases.c | sed -e 's/\.c/\.o/'` >> Makefile.flat 51cat Makefile.tmp >> Makefile.flat 52rm Makefile.tmp 53makedepend -f Makefile.flat *.c 54mv clb_defines.h tmpfile 55echo "#define NDEBUG /* Automatically added for SPEC */" > clb_defines.h 56#echo "#define SPEC_CPU2004 /* Automatically added for SPEC */" >> clb_defines.h 57echo "#define CONSTANT_MEM_ESTIMATE /* Automatically added for SPEC */" >> clb_defines.h 58echo "#define FAST_EXIT /* Automatically added for SPEC */" >> clb_defines.h 59cat tmpfile >> clb_defines.h 60rm tmpfile 61