sosy-lab/sv-benchmarks

CI for coverage properties

lembergerth opened this issue · 1 comments

Currently, coverage properties are not always updated with their corresponding formal-verification properties. So at the moment, I run a toolchain to update all of the tasks once a year.

This could be improved on with a CI check that:

  • checks that all coverage-related benchmark tasks fulfill the above criteria.
  • checks that all not-coverage-related benchmark tasks do not fulfill the above criteria.

This CI check would allows us to keep coverage-properties consistent.

Originally posted by @kfriedberger in #1209 (comment)

c/check.py already has some property-related checks including checks that ensure consistency between some properties, so I guess it would not be difficult to add it there (depending on how complex the to-be-implemented checks are).