Skip to content

goto-cc --function produces "error: failed to initialize `symbol'" #2745

Closed
@polgreen

Description

@polgreen

A change that happened in develop between yesterday and today has made yesterdays goto-cc binaries incompatible with todays goto-cc.

I am aware that goto-cc was made incompatible with goto-binaries made with versions of CBMC prior to 5.10, but these binaries were made with goto-cc post 5.10.

I have moved from CBMC at this commit (with 2 commits reverted because they cause issue #2740). Call this CBMC version 1:

df44b74 Revert "type symbols now use ID_symbol_type"
c34ba19 Revert "avoid assert()"
05993f4 Merge pull request #2727 from tautschnig/fptr-debug

To CBMC at this commit (with 2 commits reverted because of issue #2740). Call this CBMC version 2:

d1fe30e Revert "type symbols now use ID_symbol_type"
2620809 Revert "avoid assert()"
1f06cde Merge pull request #2743 from tautschnig/boolbv-width

I am using a Xen binary, which can be compiled as in the docker file in PR #2504

If the binary is created with CBMC version 1, and then the following command is made with CBMC version 2, I get the following error:

goto-cc --function x86_emulate xen-syms.binary -o output.binary
traps.c:104:1: error: failed to initialize `symbol'

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