Bug: Wrong location with RCFGBuilder

[schuessf]

Consider the following program:

void error() { 
  reach_error();
}

int main() {
  int x = 0;
  while (1) {
    if (x == 0) break;
    error();
  }
}

void unreachable() {
  error();
}

When verifying this program with Automizer in the SV-COMP settings (i.e., with RCFGBuilder), we get the following invariant (in the YAML format):

  - invariant:
      type: loop_invariant
      location:
        line: 7
        column: 13
        function: main
      value: (x == 0)
      format: c_expression

While the invariant is a valid (and inductive) loop invariant for this example, the column is wrong and therefore a witness containing such an invariant is syntactically invalid. The location should point to the "w" of while, rather than {.

After debugging this example, I figured out that the issue has to be in RCFGBuilder:
I suppose that edges for some of the statements are merged (due to preprocessing we have also many labels and gotos), but "forgets" the correct location for the loop that is later used a location in the witness. This only seems to happen for C programs containing a while loop with a body that starts with an if and ends with a call that cannot be inlined (therefore the example contains the function unreachable). Such tasks occur quite often in the SV-COMP benchmarks (~500 times in the ReachSafety category), often due to preprocessing with CIL.

If we use the IcfgBuilder instead, we get the correct location for this loop invariant (i.e., column 3). Therefore, I am not quite sure if it is woth to fix the RCFGBuilder, or if we should rather fix the remaining performance issues in IcfgBuilder use it instead.