SRI-CSL / yices2 / 25301905438

67%

master: 67%

Build Type

Pull #590

github

Committed by disteph

Commit Message

coverage: mark fail-closed defensive branches LCOV_EXCL

The four review-driven commits earlier in this PR added defensive
fail-closed branches that are unreachable on supported inputs:

  - src/mcsat/uf/uf_plugin.c
      * uf_plugin_get_function_id_from_trail's q_get32 failure path
      * uf_plugin_build_app_model_compare's both-ids-failed fallback
      * uf_model_builder_remember_function_term's early return
      * uf_model_builder_get_function_value's early return on id lookup
      * uf_model_builder_get_function_value's make_fresh_function ==
        null_value branch (rejected by the preprocessor guard)
      * uf_model_builder_prepare's continue on id lookup

  - src/context/context.c
      * two internalize_to_eterm consistency assert()s that fire only
        when root was already mapped during recursive internalization

All of these are never taken in the gcov regression run (either
guarded out by term_needs_function_diseq_guard in preprocessor.c, or
structurally impossible because function ids are allocated as small
non-negative integers by uf_plugin_decide), so they show up as
uncovered lines and regress PR 590's coveralls score.

Wrap each with LCOV_EXCL_LINE (single-line branches) or
LCOV_EXCL_START / LCOV_EXCL_STOP (multi-line blocks). The hardening
itself is preserved; the markers only tell lcov not to count these
deliberately unreachable lines against the coverage metric.

No behavior change.

Refs: PR #590, coveralls build 79245430.

Pull Request Pull Request #590: fixes #414

Coverage Stats

65 of 80 new or added lines in 6 files covered. (81.25%)

37 existing lines in 8 files now uncovered.

83456 of 125146 relevant lines covered (66.69%)

1655176.37 hits per line