Skip to content

goto-analyser simplify generates binary that can't be analyzed with goto-instrument #2689

Open
@polgreen

Description

@polgreen

I am using this Xen binary (which is a goto-cc build of this branch: https://github.com/nmanthey/xen/tree/gotocc):
https://drive.google.com/file/d/1Vco57D_iMhQ6N1EXqLTmF1wC9WiSN3mZ/view?usp=sharing
To rebuild this binary, use the docker file in this PR:
#2504

I am running the following commands:

goto-analyzer --simplify output.binary xen-syms.binary
goto-instrument --call-graph output.binary

The error message is:

goto-instrument: local_bitvector_analysis.cpp:185: local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(const exprt&, local_bitvector_analysist::points_tot&): Assertion `rhs.op0().type().id()==ID_pointer' failed.

I am running on develop + this PR: #2642.
I get the same error when I try develop + these patches:https://github.com/tautschnig/cbmc/tree/extend-simplifier.

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