runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

Abstract proof hints writer #1118

Closed theo25 closed 3 months ago

theo25 commented 3 months ago

This PR refactors the process of outputting proof hints to file so that it is handled by an abstract proof_trace_writer. We then implement a subclass of the proof_trace_writer class, namely proof_trace_file_writer, that outputs the proof hints to a binary file.

We do that so that we can easily add other methods of outputting proof hints in the future, such as a shared memory / ringbuffer based writer that will work in tandem with the shared memory proof hints parser that was recently merged.

The PR can be easily reviewed commit by commit.

theo25 commented 3 months ago

@Baltoli I don't know if you will have the time to review this one so I didn't ask for a review. If you do have the time, your comments are always welcome and appreciated!