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