Skip to content

goto-cc produces binaries that can't be analyzed #2740

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
polgreen opened this issue Aug 15, 2018 · 1 comment
Closed

goto-cc produces binaries that can't be analyzed #2740

polgreen opened this issue Aug 15, 2018 · 1 comment

Comments

@polgreen
Copy link
Contributor

using CBMC on develop at commit:
05993f4

I am compiling this branch of Xen with goto-cc, using one-line-scan as in the docker file in PR #2504:
https://github.com/nmanthey/xen/tree/gotocc

The binary is here:
https://s3.amazonaws.com/cbmc-public-bucket/xen-syms.binary

The commands I am running are:

cp xen-syms xen-syms.binary
goto-instrument --show-goto-functions xen-syms.binary

The error is:

Reading GOTO program from `xen-syms.binary'
identifier tag-#anon#UN[SYM#tag-#anon#ST[U64'l1']#'l1e'|U64'el1e'] not found

This can be temporarily fixed by removing the ID symbol change in the following commits (thanks Michael for pointing me to these)

355fbd2920e5e22cdff23a31491916e8a09c1476
f93deec812fc52c5dc3e7d4fc77f39a35e76e671
@kroening
Copy link
Member

PR #2742 is a candidate fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants