Skip to content

`flow_insensitive_invariant` YAML entry type

Simmo Saan requested to merge github/fork/goblint/flow_insensitive_invariant into main

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.

Merge request reports