|
#!/usr/bin/env bash
#
# Author: Sascha Boehme
#
# DESCRIPTION: testing tool for automated proof tools
PRG="$(basename "$0")"
function print_action_names()
{
for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML
do
echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/'
done
}
function print_sledgehammer_options() {
grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \
perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/'
}
function usage() {
# Do not forget to update the Sledgehammer documentation to reflect changes here.
[ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
timeout="$MIRABELLE_TIMEOUT"
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
echo
echo " Options are:"
echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)"
echo " -O DIR output directory for test data (default $out)"
echo " -S FILE user-provided setup file (no actions required)"
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -d DIR include session directory"
echo " -q be quiet (suppress output of Isabelle process)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
echo
echo " Apply the given actions at all proof steps in the given theory files."
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
print_action_names
echo
echo " Available OPTIONs for the ACTION sledgehammer:"
print_sledgehammer_options
echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"
echo " range the given actions are to be applied."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
[ $# -eq 0 ] && usage
MIRABELLE_DIR=
MIRABELLE_SETUP_FILE=
while getopts "L:T:O:d:t:S:q?" OPT
do
case "$OPT" in
L)
MIRABELLE_LOGIC="$OPTARG"
;;
T)
MIRABELLE_THEORY="$OPTARG"
;;
O)
MIRABELLE_OUTPUT_PATH="$OPTARG"
;;
d)
MIRABELLE_DIR="$OPTARG"
;;
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
S)
MIRABELLE_SETUP_FILE="$OPTARG"
;;
q)
MIRABELLE_QUIET="true"
;;
\?)
usage
;;
esac
done
export MIRABELLE_DIR
export MIRABELLE_SETUP_FILE
export MIRABELLE_QUIET
shift $(($OPTIND - 1))
export MIRABELLE_ACTIONS="$1"
shift
# setup
if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
PURGE_OUTPUT="true"
fi
mkdir -p "$MIRABELLE_OUTPUT_PATH"
export MIRABELLE_OUTPUT_PATH
## main
for FILE in "$@"
do
perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
done
## cleanup
if [ -n "$PURGE_OUTPUT" ]; then
rm -rf "$MIRABELLE_OUTPUT_PATH"
fi
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
