Kani's test suite requires universal-ctags but doesn't report that when the test fails

[pnkfelix]

I tried the follow command line invocation:

./scripts/kani-regression.sh

with a check out at commit 5d206d6

I expected to see this happen: A clean test suite run.

Instead, this happened: A single test failure:

[...]
subprocess.CalledProcessError: Command '['ctags', '-n', '-f', '-', '/media/pnkfelix/FormalMethods/kani/tests/cargo-kani/simple-visualize/src/main.rs']' returne\
d non-zero exit status 1.

------------------------------------------
stderr:
------------------------------------------
   Compiling simple-visualize v0.1.0 (/media/pnkfelix/FormalMethods/kani/tests/cargo-kani/simple-visualize)
    Finished dev [unoptimized + debuginfo] target(s) in 0.22s
Error: cbmc-viewer exited with status exit status: 1

------------------------------------------



failures:
    [cargo-kani] cargo-kani/simple-visualize/main.expected

Eventually I read and re-read the messages and then tried running ctags myself, and discovered that the default ctags on my machine (which I suspect emacs installed) does not support the -n option.

It would be nice if the Kani test harness detected this and asked me to install universal-ctags, rather than failing in this obscure manner.

[zhassan-aws]

Thanks for filing this issue, @pnkfelix! A newer version of CBMC viewer (which is one of Kani's dependencies) addressed the ctags issue, by adding support for multiple versions of ctags. We will bump the CBMC viewer version to bring in this fix for our next release.