Skip to content

New bug in function and refunction #21

@pwnchaser

Description

@pwnchaser

Hello,
I recently checked out https://github.com/naim-mr/refunction, the new version of function from SV-Comp26 and noticed that both function and refunction erroneously classify this program as terminating:

void f2();

void f1() {
  f2();
}

void f2() {
  while(1)
    ;
}

int main(void) {
  f1();
  return 0;
}

Meanwhile refunction does not expose anymore my previous bug report #19, so I believe this is a bug with a different root cause. Also this program does not have return statements that occur before the end of a function, so this might be something you want to look in.
Thank you!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions