Testing - runtimeverification/haskell-backend GitHub Wiki

Kore's integration tests

To run all integration tests, run make test in the test/ directory.

To execute integration tests only from one subfolder of test/, run from project root:

make -C "test/issue-2700" test

To accept new output as correct for a golden test, cd into its subdirectory, delete the golden file, and make with the golden file's name as the target.

Unit and property tests

Run unit tests that match an awk pattern:

stack test --test-arguments '--pattern "$(NF-1) ~ /Set/ && $NF ~ /matches/ "'

Here we run test that has Matcher in its module name ($0) and Set in its test group ($(NF -1)). NF stands for Number of Fields, i.e. $NF is the last field in the test table, which is the test name from the source file.

Add a -l before the last double quotation mark to list the tests without running them.

One can also do the same with cabal:

cabal run kore-test -- --pattern '$(NF-1) ~ /Set/ && $NF ~ /matches/'

Modifying the regression tests

  1. Modify generate-regression-tests.sh, adding or modifying regression tests under generate-evm() and generate-wasm() as necessary.

  2. Run the now modified generate-regression-tests.sh on your machine.

  3. In the test directory, run make golden.

  4. Commit the changes you've made to the script, all updated test files, and all updated golden files to your branch.