Better error message for missing dependencies

[feliperodri]

One user reporter the following error while trying to run the run-cbmc-proofs.py script.

./run-cbmc-proofs.py --proofs aws_byte_buf_append_and_update

For your convenience, the output of this run will be symbolically linked to  /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/output/latest/html/index.html

Configuring CBMC proofs: 1 / 1
[2/17] aws_byte_buf_append_and_update: building project binary                                                                            /Users/graebm/dev/aws-c/aws-c-common/source/allocator.c:258:1: warning: function '__builtin___CFStringMakeConstantString' is not declared

 static CFStringRef s_cf_allocator_description = CFSTR("CFAllocator wrapping aws_allocator.");

[17/17] aws_byte_buf_append_and_update: generating report                                                                                 FAILED: /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/report /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/output/litani/runs/a6cc463e-e4fc-4c6b-a3c7-8aca70e26612/status/c0f0b5ab-ce23-4628-b039-d869bb3008bc.json

/usr/local/Cellar/litani/1.28.0/libexec/litani exec --command 'cbmc-viewer --result /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/result.xml --coverage /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/coverage.xml --property /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/property.xml --srcdir /Users/graebm/dev/aws-c/aws-c-common --goto /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/gotos//Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/aws_byte_buf_append_and_update_harness.c.goto --reportdir /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/report --config /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/cbmc-viewer.json' --pipeline-name aws_byte_buf_append_and_update --ci-stage report --job-id c0f0b5ab-ce23-4628-b039-d869bb3008bc --stdout-file /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/viewer-log.txt --description 'aws_byte_buf_append_and_update: generating report' --status-file /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/output/litani/runs/a6cc463e-e4fc-4c6b-a3c7-8aca70e26612/status/c0f0b5ab-ce23-4628-b039-d869bb3008bc.json --profile-memory-interval 10 --inputs /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/result.xml /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/property.xml /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/logs/coverage.xml --outputs /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/report

/bin/sh: /usr/local/bin/cbmc-viewer: /usr/local/Cellar/cbmc-viewer/3.8/libexec/bin/python3.8: bad interpreter: No such file or directory

litani: Output file '/Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/report' of pipeline 'aws_byte_buf_append_and_update' did not exist upon job completion. Not copying to artifacts directory. If this job is not supposed to emit the file, pass `--phony-outputs /Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/aws_byte_buf_append_and_update/report` to suppress this warning

ninja: build stopped: cannot make progress due to previous errors.


Report was rendered at file:///Users/graebm/dev/aws-c/aws-c-common/verification/cbmc/proofs/output/latest/html/index.html

I believe they don't have cbmc-viewerinstalled. If that's the case, we need better error messages to point users for the installation pages.

[graebm]

It's me, I'm the user

tldr; seems like cbmc-viewer is trying to use python3.8, without explicitly depending on it

here's my investigative journey..

---

I did have cbmc-viewer installed via homebrew. I just now tried re-installing it, to see if that would magically fix it, but I'm seeing the same error when running cbmc-viewer directly:

$ cbmc-viewer --version
zsh: /usr/local/bin/cbmc-viewer: bad interpreter: /usr/local/Cellar/cbmc-viewer/3.8/libexec/bin/python3.8: no such file or directory

So I decided to trace what's up with that python3.8 call..

$ ls -l /usr/local/Cellar/cbmc-viewer/3.8/libexec/bin/python3.8
lrwxr-xr-x  1 graebm  admin  84 Dec 16 10:03 /usr/local/Cellar/cbmc-viewer/3.8/libexec/bin/python3.8 -> ../../../../../opt/[email protected]/Frameworks/Python.framework/Versions/3.8/bin/python3.8

ah, there are some softlinks, let's follow them...

$ realpath /usr/local/Cellar/cbmc-viewer/3.8/libexec/bin/../../../../../opt/[email protected]
/usr/local/opt/[email protected]

~$ ls -al /usr/local/opt/[email protected]                                                    
ls: /usr/local/opt/[email protected]: No such file or directory

yeah, there's no /usr/local/opt/[email protected]. Let's see if some other python shortcuts are there...

$ ls -al /usr/local/opt/python*
lrwxr-xr-x  1 graebm  admin  28 Apr 17 11:31 /usr/local/opt/python@3 -> ../Cellar/[email protected]/3.11.3
lrwxr-xr-x  1 graebm  admin  29 Apr 17 11:46 /usr/local/opt/[email protected] -> ../Cellar/[email protected]/3.10.11
lrwxr-xr-x  1 graebm  admin  28 Apr 17 11:31 /usr/local/opt/[email protected] -> ../Cellar/[email protected]/3.11.3
lrwxr-xr-x  1 graebm  admin  27 Jan 10 14:28 /usr/local/opt/[email protected] -> ../Cellar/[email protected]/3.9.16

so I tried installing python3.8 via homebrew, and that fixed it!

$ brew install [email protected]

$ cbmc-viewer --version
CBMC viewer 3.8