Mark synthetic locations

[sim642]

This adds the field synthetic to Cil.location and allows locations for CIL-synthetized statements to be marked as such. It allows Goblint to avoid generating invalid invariants for such locations.

This is kind of ugly, but I don't know how we could do any better, since for invariant generation we need to know about legal locations in the untransformed source.

Examples

for loop

for(x = 0; x < 10; x++) {
  // ...
}

As the for loop is transformed by CIL, x = 0, x < 10 and x++ are all given the location of the loop itself, i.e. immediately before the keyword for.
Since these statements end up corresponding to vastly different CFG nodes, it's incorrect to insert invariants from all of them before the loop.

expression with side effect

i = k = 0;

CIL transforms this expression into two statements: k = 0 and i = k, both of which are given the location of the entire original statement.
This means that the invariant for the state between the two assignments is located before the entire statement, which is incorrect.
synthesizeLocs is used to transform expression side-effect chunks to have synthetic intermediate locations (but keep the first location as non-synthetic). This applies to any kind of expression decomposition, including function calls, etc.

compound initializers

struct kala {
  int kaal;
  int hind;
};

struct kala a = {2,3};

CIL transforms this initializer into two statements: a.kaal = 2 and a.hind = 3. Again, it is impossible to reference program points between these, so synthesizeLocs takes care of them as well.

[michael-schwarz]

👍