Support YAML violation witnesses

[schuessf]

This PR adds support for violation witnesses in the YAML format. The main work (thanks to @HelenAnnaMeyer) was the following:

• Add AST objects for the new witness format
• Allow Parsing violation witnesses from YAML (extend YamlWitnessParser).
• Generate AST object to represent violation witnesses from an IProgramExecution (see YamlViolationWitnessGenerator)
• Validate violation witnesses (see YamlWitnessProductAutomaton): Create a product automaton of a program automaton and a witness to use this product as as the initial abstraction in the verification (TraceAbstraction / BüchiAutomizer).

In order to work properly, this required the following additional changes:

• Add WitnessTransformer as an abstraction for violation witnesses in YAML and GraphML
• Slightly adapt our C-translation (see CHandler) for loops to extract the correct branching condition for the witnesses
• Add methods to get the required infos (line, column, function) for the witness to IBacktranslationValueProvider

There are still some issues / open questions:

• Some of the added regression tests currently fail, because of bugs in the RCFGBuilder. They should however work properly, if the IcfgBuilder is used instead (i.e., once this branch is merged).
• Currently we don't generate any assumptions from our counterexamples. We could get them from our program states (there is already the class ProgramStatePrinter for this), but we currently only get states at locations that are not legal for assumptions according to the format. This might also change with the usage of IcfgBuilder.
• We currently cannot check the assumptions during validation (which happens in the trace abstraction), as this would require to translate them from C to SMT (which has to be done in the translation and not only in the trace abstraction). However, we currently try to validate at least the location of the assumptions. This might however be problematic if we use large block encoding (as no matching edge might exist for the C statement), therefore there is a boolean flag CHECK_ASSUMPTION_LOCATIONS in YamlWitnessProductAutomaton. We need to figure out the best "mode" for validation (combination of block encoding and this flag), especially for the SV-COMP.
• Witness generation and validation is only properly tested for ReachSafety. However, I just tested generation and validation for simple examples for NoOverflow and MemSafety, and it seems to work in principle. This might require some further testing for SV-COMP.

For SV-COMP, we still need to add a benchdef for violation witnesses 2.0, once this PR is merged.

[maul-esel]

Looks good, thanks @HelenAnnaMeyer and @schuessf for adding this support!

I've left some smaller comments. I also remember in our discussion after the presentation, it was mentioned that some aspects of the semantics of violation witnesses were not entirely clear (though I forgot what it was). Should we take this up with the authors / at SV-COMP before merging this, or do you think it's better to work with the current implementation and, if necessary, make changes later on?

[bahnwaerter]

I quickly skimmed through the changes and they look good so far. I have also noted a few minor things. You could also consider removing personal data from the example witnesses. This affects in particular the encoding of the user name in the file path of the specified witness files in the metadata section of each witness file.

[bahnwaerter]

There is some indentation issue. Is this the result of an unfavorable formatter setting?

[schuessf]

Yes, but this might have been fixed now, this was before the Java 21 migration, where we also slightly adapted the formatter. I will just keep this for now, we will run the formatter anyway on the dev branch.

[bahnwaerter]

Another example of an unfavorable formatter setting?