Call elimination: requires violation diagnostic should point to call site

[fabiomadge]

Problem

When a requires precondition is violated at a call site, the diagnostic points to the requires expression (the callee's definition), not the call site where the violation occurs.

Laurel example:

procedure takesPositive(n: int) returns (r: int)
  requires n > 0
{
  return n;
}
procedure caller() returns (r: int) {
  var x: int := takesPositive(-1);
  return x;
}

The error points to n > 0 on line 2 (the requires clause) rather than takesPositive(-1) on line 7.

Root cause

Core's call elimination (CallElim) inlines the contract at each call site by generating assert requires_expr. The metadata on the generated assert comes from the requires expression, so the diagnostic points to where the requires was defined, not where it was violated.

Proposed fix

In CallElim, when generating the assert for a requires check at a call site, use the call site's metadata instead of (or in addition to) the requires expression's metadata.