I think we might want options like trans.assert.only-at-locks which the assert transformation currently has, to also apply to these YAML witnesses. Ideally these wouldn't also duplicate witness.invariant.nodes.

So the question is, what prefix to use for such unified options? Maybe witness.invariant is the appropriate thing and we could consider the assert-annotated C programs also a custom witness format (and thus move/rename the trans.assert options there). Thoughts, @michael-schwarz?

and thus move/rename the trans.assert options there

Yes, I think that would make sense!

trans.assert.only-at-locks also apply to these YAML witnesses

Yes, that is a sensible option! However, I am a bit dubious as to how you would achieve this when the dumping of yaml witnesses is not formulated as a transformation of the AST where the AST is easily at hand.

However, I am a bit dubious as to how you would achieve this when the dumping of yaml witnesses is not formulated as a transformation of the AST where the AST is easily at hand.

I don't think it's any harder because Statement nodes still provide direct access to the Cil.stmt. It might even be simpler because there's no need to manipulate CIL's instr lists and CFG edges are even more similar with how the analysis itself recognizes locks.

This should be more reliable overall since AST transformations can only do queries based on Cil.location, the mapping of which to a node isn't directly possible.