More precise `[llvm]`/`[cached *]` log context

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework

BSD 3-Clause "New" or "Revised" License

204 stars 39 forks source link

More precise `[llvm]`/`[cached *]` log context #3957

Closed geo2a closed 1 week ago

geo2a commented 1 week ago

We emit a log message upon getting the result of an LLVM backend call, but we do not have a message that would give us the precise term we send. This PR fixes that.

goodlyrottenapple commented 1 week ago

We now emit correct messages for cached llvm/equation applications:

...[term 8d2fa91][kore-term] lengthBytes(_)_BYTES-HOOKED_Int_Bytes(buf("32", VarCONTRACT_ID:SortInt{}))
...[term 8d2fa91][success][cached equations][term 5a54a11][kore-term] "32"