configure

#!/bin/sh

usage () {
cat <<EOF
usage: configure [ <option> ... ]

where '<option>' is one of the following:

-h | --help             print this command line option summary
-g | --debug            include symbol table, logging and checking code
                       
-c | --check            include internal checking code (forced by '-g')
-l | --logging          include internal logging code (forced by '-g')
-s | --symbols          include symbol table (forced by '-g' useful without)
-p | --pedantic         pedantic compilation ('-Werror -std=c99 --pedantic')
-d | --diagnose         print compiler options (compiler pragma messages)
                       
--no-check              disable checking code (for '-g')
--no-logging            disable logging code (for '-g')
                 
-f... | -static         passed to compiler (like '-fsanitize=address')

EOF

# The main feature options are in the following generated file.

. features/usage.sh
}

############################################################################

# Terminal colors for fancy output.

if [ -t 1 ]
then
  BOLD="\033[1m"
  NORMAL="\033[0m"
  RED="\033[1;31m"
fi

die () {
  echo "${BOLD}configure: ${RED}error:${NORMAL} $*" 1>&2
  exit 1
}

############################################################################

# Basic options.

debug=no
check=undefined
logging=undefined
symbols=no
pedantic=no
diagnose=no

# Options to disable features (see also 'OPTIONS.md').

. features/init.sh

# Additional options such as '-f...'.

options=""

############################################################################

. features/parse.sh
. features/only.sh

config="$0"

while [ $# -gt 0 ]
do
  case "$1" in

    --default) ;;

    -h|--help) usage; exit 0;;

    -g|--debug) debug=yes;;
    -c|--check) check=yes;;
    -l|--logging) logging=yes;;
    -s|--symbols) symbols=yes;;
    -p|--pedantic) pedantic=yes;;
    -d|--diagnose) diagnose=yes;;

    --no-check)
      [ $check = yes ] && \
        die "can not combine '--check' and '--no-check'"
      check=no
      ;;

    --no-logging)
      [ $logging = yes ] && \
        die "can not combine '--logging' and '--no-logging'"
      logging=no
      ;;

    -f*|-static) options="$options $1";;

    --only-*) only "$1" || die "invalid option '$1' (try '-h')";;
    --no-*) parse "$1" || die "invalid option '$1' (try '-h')";;
  esac
  config="$config $1"
  shift
done

############################################################################

rm -f .config || exit 1
echo "$config" > .config

############################################################################

. features/check.sh

# All checks of incompatible options.

[ $debug = yes -a $check = yes ] && \
  die "'--debug' implies '--check'"

[ $debug = yes -a $logging = yes ] && \
  die "'--debug' implies '--logging'"

[ $debug = yes -a $symbols = yes ] && \
  die "'--debug' implies '--symbols'"

[ $debug = no -a $check = no ] && \
  die "can not use '--no-check' without '-g'"

[ $debug = no -a $logging = no ] && \
  die "can not use '--no-logging' without '-g'"

############################################################################

CC=gcc

CFLAGS="-W -Wall"
[ $pedantic = yes ] && CFLAGS="$CFLAGS -Werror -std=c99 --pedantic"

if [ $debug = yes ]
then
  CFLAGS="$CFLAGS -ggdb3"
else
  CFLAGS="$CFLAGS -O3"
fi

# Here come the options which disable certain code features mostly for
# didactic purposes in order to show the effect of certain ideas.

[ $symbols = yes ] && CFLAGS="$CFLAGS -ggdb3"
CFLAGS="$CFLAGS$options"

[ $check = undefined ] && check=$debug
[ $logging = undefined ] && logging=$debug

[ $check = no ] && CFLAGS="$CFLAGS -DNDEBUG"
[ $logging = yes ] && CFLAGS="$CFLAGS -DLOGGING"
[ $diagnose = yes ] && CFLAGS="$CFLAGS -DIAGNOSE"

. features/define.sh

COMPILE="$CC $CFLAGS"
echo "$COMPILE"

############################################################################

rm -f makefile
sed "s#@COMPILE@#$COMPILE#" makefile.in > makefile

# Removes the proof checker dependencies in the generated 'makefile' if
# checking is disabled.

if [ $check = no ]
then
  sed "s#@COMPILE@#$COMPILE#" makefile.in | \
  sed '/^catch.o/d;s, catch.o,,' > makefile
else
  sed "s#@COMPILE@#$COMPILE#" makefile.in > makefile
fi