Fixed error reporting in the verifier

[cmnrd]

This PR fixes several issues related to error reporting in the verifier.

• The verifier was invoked in LFGenerator. This led to the problem that GeneratorBase cleared all reported errors after the verifier run (See this comment). This is fixed by moving the invocation of the verifier to GeneratorBase.
• If something went wrong while running uclid, the verifier code would simply exit. This led to the problem that the verifier tests abort without any indication of why (See this CI run). The verifier now correctly reports the error using our message reporter.
• The PR also includes several cleanups.

[lsk567]

Thanks for working on this, Christian. Looks good to me!

I can confirm this is working on my Mac machine, including when one of the dependencies is not installed.

[lsk567]

One minor point is the time measurement doesn't seem working. The tests all take 0 time to complete.

    ------------------------------------------------------------------------------
    Covered: 13/13
    ------------------------------------------------------------------------------

    ------------------------------------------------------------------------------
    Passing: 12/13
    ------------------------------------------------------------------------------
    Passed: src/verifier/AircraftDoor.lf in 0.00 seconds
    Passed: src/verifier/Alarm.lf in 0.00 seconds
    Passed: src/verifier/CoopSchedule.lf in 0.00 seconds
    Passed: src/verifier/Election2.lf in 0.00 seconds
    Passed: src/verifier/PingPongVerifier.lf in 0.00 seconds
    Passed: src/verifier/ProcessMsg.lf in 0.00 seconds
    Passed: src/verifier/ProcessSync.lf in 0.00 seconds
    Passed: src/verifier/Ring.lf in 0.00 seconds
    Passed: src/verifier/SafeSend.lf in 0.00 seconds
    Passed: src/verifier/Thermostat.lf in 0.00 seconds
    Passed: src/verifier/TrainDoor.lf in 0.00 seconds
    Passed: src/verifier/UnsafeSend.lf in 0.00 seconds
    ------------------------------------------------------------------------------
    +---------------------------------------------------------------------------+
    Failed: src/verifier/ADASModel.lf in 0.00 seconds

The failure case is artificially injected. No need to worry about it.

[lhstrh]

Heads up: this will clash with my refactoring in #2008.

[lhstrh]

The failure case is artificially injected. No need to worry about it.

What do you mean? If it fails the whole test doesn't pass. Are you saying it should not be marked as failing?

[lsk567]

The failure case is artificially injected. No need to worry about it.

What do you mean? If it fails the whole test doesn't pass. Are you saying it should not be marked as failing?

I meant I changed the test on my local branch to make it fail, so that I can observe whether the test harness can catch it. And it did successfully. The version on the remote is still passing.

[cmnrd]

I think the reported times are execution times of the binary program. For the verifier tests, we only build and do not run the tests, so I guess this explains the numbers.