Skip to content

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

Closed
@polgreen

Description

@polgreen

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions