Is ctags required?

[tedinski]

The releases documentation says:

For best results, install universal ctags or exuberant ctags with

(Emphasis mine.) It doesn't seem like it's meant to be required. (Though on second read, maybe it's recommending a better version of ctags vs the usual one?)

But when I invoke viewer like the following, in a docker container with minimal dependencies:

cbmc-viewer
  --result cbmc-for-foo.results.xml
  --coverage cbmc-for-foo.coverage.xml
  --property cbmc-for-foo.property.xml
  --srcdir .
  --wkdir .
  --goto cbmc-for-foo.out
  --reportdir report-foo

I get this traceback:

WARNING: Property name not of the form STRING.INTEGER: 1
ERROR: Skipping reachable function with invalid source location: {'function': '', 'lastLine': 4}
ERROR: Skipping reachable function with invalid source location: {'function': '_17631127924912787913::vtable_impl_for__8528040594070026755_init'}
Traceback (most recent call last):
  File "/tmp/kani/kani-latest/pyroot/bin/cbmc-viewer", line 8, in <module>
    sys.exit(viewer())
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/viewer.py", line 202, in viewer
    symbols = symbolt.make_symbol(args.viewer_symbol, args.viewer_source,
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/symbolt.py", line 267, in make_symbol
    return SymbolFromGoto(goto, wkdir, srcdir)
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/symbolt.py", line 144, in __init__
    file_symbols = symbols_from_files(goto, wkdir, srcdir)
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/symbolt.py", line 141, in symbols_from_files
    return SymbolFromCtags(srcdir, files).symbols
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/symbolt.py", line 112, in __init__
    parse_ctags_data(run_ctags(root, files), root)
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/symbolt.py", line 196, in run_ctags
    ctags_output = runt.run(
  File "/tmp/kani/kani-latest/pyroot/cbmc_viewer/runt.py", line 40, in run
    result = subprocess.run(cmd, **kwds, check=False)
  File "/usr/lib/python3.8/subprocess.py", line 493, in run
    with Popen(*popenargs, **kwargs) as process:
  File "/usr/lib/python3.8/subprocess.py", line 858, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "/usr/lib/python3.8/subprocess.py", line 1704, in _execute_child
    raise child_exception_type(errno_num, err_msg, err_filename)
FileNotFoundError: [Errno 2] No such file or directory: 'ctags'

Is ctags required actually (release text should probably be updated if so), or is this a bug?

(I'm also not clear on what viewer is using ctags for... is this possibly pointless for Kani/Rust code? Is there an option we can supply to avoid using ctags?)

[space-miner]

afaik ctags is a dependency.

[tedinski]

If so, then some documentation needs updating. Besides the release notes I mentioned above:

https://model-checking.github.io/cbmc-viewer/installation/

The installation of ctags is optional

[markrtuttle]

The installation of ctags should be optional. What will be lost is linking to source code definitions for symbols found by ctags that do not appear in the symbol table of the goto binary (eg, types). The choice between exhuberant ctags and universal ctags should be optional, but the installation of universal ctags is preferred because, for example, it supports rust symbols. I will look into whether recent changes have implicitly assumed ctags or universal ctags.