Skip to content

goto-instrument --dump-c produces incorrect results if the code has been unwound or inlined #226

Open
@martin-cs

Description

@martin-cs

The following sequence is needed to reproduce the bug:

goto-cc original.c -o original.goto
goto-instrument --unwind 4 original.goto original-unwound.goto
goto-instrument --dump-c original-unwound.goto

In the case of unwinding, dump-c produces multiple copies of variable definitions and does not correctly translate the later loop bodies (omitting function calls). If --inline is used instead of --unwind the result doesn't appear to be valid C.

I have full example code if anyone wants a go at fixing this but because github sucks I can't actually attach it to this bug report.

@tautschnig

Activity

added a commit that references this issue on Oct 5, 2017

Merge pull request diffblue#226 from diffblue/feature/goto_statistics

added a commit that references this issue on Jan 16, 2018

Merge pull request diffblue#226 from diffblue/feature/goto_statistics

added a commit that references this issue on Aug 24, 2018

Merge pull request diffblue#226 from diffblue/issue205

c6ec14f
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @peterschrammel@martin-cs

        Issue actions

          goto-instrument --dump-c produces incorrect results if the code has been unwound or inlined · Issue #226 · diffblue/cbmc