Added a pass that warns about loops

[shaobo-he]

It also prints a loop bound if it can be determined via LLVM's ScalarEvolution class. Specifically, it's equal to the ConstantMaxBackedgeTakenCount.

Partially addressed #760

[zvonimir]

I don't quite understand what this pass does. Could you add extensive comments into the pass describing what exactly it does? Also, copy them here too. Thx!

[shaobo-he]

I don't quite understand what this pass does. Could you add extensive comments into the pass describing what exactly it does? Also, copy them here too. Thx!

Sorry for the confusion. I should've made it clear. Let me explain it here and I can distill it as comments later on.

This pass is to warn users about the existence of loops since they can lead to false negatives when the specified loop unrolling bound is too low.

Let's take one of JJ's regressions as an example,

int main(void) {
  int a = 1;
  while (a < 10) {
    if (a == 5)
      break;
    a++;
  }
  assert(a != 5);
  return a;
}

If we run SMACK with the default loop unrolling bound, we'll not see the assertion failure reported because of insufficient loop unrolling. With this pass, users will get a warning message as follows,

SMACK warning: found loop from line 9 to line 13 in function main with known loop bound 4; please check loop unrolling bound otherwise there may be missed bugs;

This message is intended to remind the users to check if the loop unrolling bound is above 4 to avoid missed bugs.