formalsec / smtml / 425

44%

Build Type

push

github

Committed by filipeom

Commit Message

Refactor exception handling in operator evaluation

Previously, during operator evaluation we would raise generic failures
for following three reasons:

- A theory was unsupported
- An operator was not supported by a given theory, and
- A failure in the evaluation of an operator

This would make exception handling difficult for apps that need to
gracefully handle failures. For this reason, we refactored the above
exceptions to instead raise a `Eval_error` of type `error_kind`.

Additionally, the refactor included:

- Fixing a couple of bugs when raising the `Type_error` exception.
- Adding all the helpers used for value coercion at the top of the file.
  I think it's more organised this way. Only time will tell.

BREAKING: Exception API changed for the `Eval` module

Run Details

213 of 273 new or added lines in 1 file covered. (78.02%)

286 existing lines in 5 files now uncovered.

879 of 1925 relevant lines covered (45.66%)

7.5 hits per line