`flow_insensitive_invariant` YAML entry type
This depends on #61 being merged, the PR diff currently isn't nice, but a nicer diff can be seen here: https://github.com/sim642/sv-witnesses/compare/yaml-schema...goblint:sv-witnesses:flow_insensitive_invariant.
While loop invariants and location invariants (#62) are associated with particular program locations where the program flow reaches, there are also flow-insensitive invariants which hold throughout the program execution. This location-less entry type is just for that.
In Goblint we could particularly use these for such invariants in multithreaded programs: https://github.com/goblint/analyzer/pull/830.
TODO
-
The invariant_certificate
entry type from #62 would also apply to these, but I've avoided duplicating the same generalization here.