Location fixes for YAML witness generation/validation

[sim642]

Closes #1355.

Changes

1. Adapt compilation to location fixes from Location fixes for Goblint YAML witness generation/validation cil#167.
2. Deduplicate witness node identification logic to WitnessUtil. This prevents various copies going out of sync and makes them easier to test.
3. Extend the CFG cram test output with information about witness node identification. This makes it easy to see which CFG nodes can have which witness invariants.
4. Fix loop invariant locations. Loop heads for witnesses are not identified by back edges in CFG, but by checking for the Loop statement in the corresponding CIL AST. Loop statements are not part of our CFG nodes, so this lookup happens through skippedByEdge. This has two benefits:
   1. Loop invariants are no longer emitted for goto-loops. This matches YAML witness specification.
   2. Locations for loop heads now correctly point to the beginning of the structural loop keyword. This also works for do-while loops because the Loop node contains the location for the do.
5. Fix location for first initializer assignment. Previously initializer assignments in declarations used expression locations in the middle of the statement. Now the first assignment has its location before the entire declaration, which is a valid point before any initializers execute.
6. Make precondition_loop_invariant match loop nodes not arbitrary location nodes. This is our thing and not really used for anything, but at least the name matches the behavior now. This is from the time when loop_invariant was confused with location invariants in YAML witness specification.
7. Mark YAML witnesses incompatible with loop unrolling for now.

TODO

• Merge Location fixes for Goblint YAML witness generation/validation cil#167.

• Fix GobView semantic search test.

• Cannot have location_invariant right before loop because we have no non-loop-head node there. This meant our existing witness tests had to be changed to loop_invariants which make more sense. But our inability to have location invariants before loops could also turn out to be problematic.

  int i = 0;
  // we have no node here to attach i == 0 to
  while (i < 10)
    i++;

  Delegated to Cannot have location_invariant before loop in witness #1391.

• Adapt to Record statement copies during loop unrolling #1403.

• Merge Adapt to CfgBidirSkip gobview#44.

[michael-schwarz]

I think it's a step forward, there are a few things that we should still discuss before merging though.
It might make sense to pull out the loop unrolling and sv-comp default config discussion and discuss that separately?

[michael-schwarz]

@jerhard How does this change affect our planned usage for precondition invariants for the project with LMU? We need general precondition invariants there iirc?

[sim642]

Having precondition_location_invariant entries is just a matter of defining the corresponding types and doing what we already have for location_invariant vs loop_invariant: use a different predicate for filtering nodes.

[sim642]

It might make sense to pull out the loop unrolling and sv-comp default config discussion and discuss that separately?

It's now extracted to #1402.