Skip to content

Commit

Permalink
kat: simplify functionality
Browse files Browse the repository at this point in the history
  • Loading branch information
Everett Hildenbrandt committed Mar 3, 2019
1 parent 3245b44 commit 14ed0d3
Showing 1 changed file with 7 additions and 30 deletions.
37 changes: 7 additions & 30 deletions kat
Original file line number Diff line number Diff line change
Expand Up @@ -61,23 +61,10 @@ run_program() {
fi
}

run_kdebug() {
local run_file strategy
run_file="$1" ; shift
strategy="$1" ; shift
run_krun "$run_file" "$strategy" --debugger "$@"
}

run_ksearch() {
local run_file strategy
run_file="$1" ; shift
strategy="$1" ; shift
run_krun "$run_file" "$strategy" --search "$@"
}

run_test() {
local test_name test_ext test_file test_strat test_out test_expected
local exec_strategy exit_status

test_name="$1" ; shift
exit_status='0'

Expand Down Expand Up @@ -123,33 +110,23 @@ run_command="$1" ; shift
case "$run_command" in

# Running
run) run_program "$@" ;;
debug) run_kdebug "$@" ;;
search) run_ksearch "$@" ;;
run) run_program "$@" ;;

# Testing
test) run_test "$@" ;;

*) echo "
usage: $0 [run|debug|search] <file> <strategy> <K args>*
usage: $0 run <file> <strategy> <K args>*
$0 test <test_name>
# Running
# -------
$0 run <pgm> <strategy> Run a single program using given strategy
$0 debug <pgm> <strategy> Run a single program using given strategy in the debugger
$0 search <pgm> <strategy> Search a single program's executions using given strategy
$0 run: Run a single program using given strategy
$0 test: Test that running a program with given strategies produces the correct output.
Note: <pgm> is a path to a file containing a program (languages supported: IMP, FUN).
<strategy> is a term in sort STRATEGY.
If `STRATEGY == orig`, then it runs with the *original* semantics under the OCaml backend.
# Testing
# -------
$0 test <pgm> <hash> Test that running with `run-orig` produces the correct hash.
Note: <pgm> is the path to the program in `tests/`
<hash> is the expected md5sum of the output
Note: This command is more for devs and CI servers.
<test_name> name of a test in `tests/imp` or `tests/fun` without extension, eg. `tests/imp/collatz`.
" ; exit ;;
esac

0 comments on commit 14ed0d3

Please sign in to comment.