sematic: Verification of return within conditionals in function

[sangisos]

Verify that a return statement is reached in functions of non-void return type.

simplified from noisy/advanced/eval.c

// Calls to expr only had the values 0,1 and 2
int expr(int l) {
  int a;
  if (l==0) {
    return a;
  }
  else if (l==1) {
    return a;
  }
  else if (l == 2) {
    if (a<0) {
      return a;
    } 
    else if (!a) {
      return 0;
    }
    else {
      return a;
    }
  }
  // panic
  // return -1;
}

int main(void) {
  expr(0);
}

A decision has been made to require non-void returning functions to reach a return statement for every possible execution path, to disallow uses that may result in unspecified behaviour.

$ gcc -c -Wall noisy/advanced/eval.c 
noisy/advanced/eval.c: In function ‘expr’:
noisy/advanced/eval.c:115:1: warning: control reaches end of non-void function [-Wreturn-type]
 }
 ^

$ clang -c -Wall noisy/advanced/eval.c 
noisy/advanced/eval.c:115:1: warning: control may reach end of non-void function
      [-Wreturn-type]
}
^
1 warning generated.

[mewmew]

Marked as a future ambition. Closing for now.

In the future, it would be very interesting to explore the possibility of utilizing symbolic execution to perform a more in-depth reach-analysis. Similarly, we may chose to explore the potential of utilizing constraint solvers to prove various aspects that may be of interest during compilation (such as bounds analysis).