search

runtimeverification / llvm-backend

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

update llvm-kompile-compute-loc and llvm-kompile-compute-ordinal #1094

Closed dwightguth closed 2 weeks ago

dwightguth commented 3 weeks ago

These binaries were not quite feature-complete with their original intended purpose, probably primarily because at the time at which they were reimplemented, the past version of them was somewhat broken.

This PR adds the following features:

  1. Outputting the k location is the default in llvm-kompile-compute-loc
  2. If a k location does not exist, it falls back to the kore location rather than crashing.
  3. The output is formatted with both a filename and a line number.
  4. In llvm-kompile-compute-ordinal, you can specify a filename and it will search for the ordinal of a k rule on that line of that file in the input definition.