search

runtimeverification / llvm-backend

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

Shared memory writer for proof hints #1122

Closed theo25 closed 3 months ago

theo25 commented 3 months ago

This PR adds a subclass of the abstract proof_trace_writer for outputting hints into a ringbuffer that lives in shared memory. This output method is intended to be used with the shared memory option of the kore-proof-trace parser to communicate hints through shared memory instead of through a file.

Since we now can test the shared memory based proof generation/consumption loop, we also do not include the helper kore-proof-trace-shm-writer tool in the installation.