Possible soundness bug in FuncTion

[pwnchaser]

Hello,
I recently installed FuncTion and noticed that it erroneously classifies this program as terminating:

int identity(int val){
  if (1)
    return val;
  else
    return val;
}

int main() {
  int c = identity(0);
  while(c == 0) {
  }
  return 0;
}

I built the latest version of FuncTion but had to switch to apron version 0.9.14, the latest version 0.9.15 triggered build errors.
Thanks in advance :)

[caterinaurban]

Thank you for the report. This an issue I am already aware of but I did not yet have the time to fix it. The problem is in the inlining, which does not correctly handle return statements that occur before the end of a function. We are working on a new version of the tool that should fix all of these issues, but it will take a while to deploy. Sorry for the wait!