search

runtimeverification / llvm-backend

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

Remove sentinel for end of KORE terms in the proof hint format #1076

Closed theo25 closed 1 month ago

theo25 commented 1 month ago

This PR removes the sentinel at the end of a KORE terms as it would appear in the proof hint trace. We do not need this sentinel to properly parse the trace because the KORE term binary format includes length information.

The hints version has been bumped to 11 and the relevant tests have been updated.

dwightguth commented 1 month ago

As Theo mentioned on slack, we are keeping the 0xFFFFFFFFFFFFFFFF sentinel because it is actually used by the parser to determine how parsing should proceed.