Skip to content

Improve property checks for coverage properties

Thomas Lemberger requested to merge improve-property-checks-for-coverage into main

In the past, some C tasks got the expected verdict of property unreach-call fixed to 'true', but property coverage-error-call was not removed. It should be because it is not possible to create a test whose execution covers an infeasible error call.

To avoid that this happens again, this MR not only fixes the inconsistencies, but adds the inconsistency checks to the CI.

There are two new checks based on properties:

  1. coverage-error-call can only exist if unreach-call exists and has expected_verdict: false
  2. coverage-branches can only exist if the program always terminates (i.e., no termination: false)

Merge request reports