search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Issues with absolute paths in srcloc. #45

Closed vecchiot-aws closed 2 years ago

vecchiot-aws commented 3 years ago

Running rmc --visualize fixme_catch_unwind.rs on this file leads to the following error in the visualizer:

Traceback (most recent call last):
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc-viewer", line 33, in <module>
    sys.exit(load_entry_point('cbmc-viewer', 'console_scripts', 'cbmc-viewer')())
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/viewer.py", line 213, in viewer
    report.report(config, sources, symbols, results, coverage, traces,
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/report.py", line 60, in report
    markup_trace.Trace(name, trace, symbols, properties, loops, snippets).dump(
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/markup_trace.py", line 103, in __init__
    self.prop_srcloc = format_srcloc(properties.get_srcloc(name)
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/markup_trace.py", line 153, in format_srcloc
    markup_link.link_text_to_file(fyle, fyle, from_file),
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/markup_link.py", line 51, in link_text_to_file
    path = path_to_file(to_file, from_file)
  File "/Users/vecchiot/Documents/aws-viewer-for-cbmc/cbmc_viewer/markup_link.py", line 34, in path_to_file
    raise UserWarning(
UserWarning: /Users/vecchiot/Documents/rmc/library/std/src/panicking.rs != ../../../../library/std/src/panicking.rs

This appears to be an issue when srcloc['file'] is an absolute path in markup_link.py.

vecchiot-aws commented 3 years ago

See #276 on RMC.

markrtuttle commented 3 years ago

Because RMC encode physical absolute paths in source locations, the invocation of cbmc viewer on RMC output must use physical absolute paths for srcdir and wkdir. I suspect that the script is invoking viewer with logical absolute paths.

markrtuttle commented 2 years ago

I consider this issue closed by https://github.com/model-checking/cbmc-viewer/pull/47