search

runtimeverification / llvm-backend

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

Un-nest proof hint events for arguments of functions/hooks #1140

Closed theo25 closed 2 months ago

theo25 commented 2 months ago

The events that correspond to evaluation of arguments of functions and hooks are currently nested inside the corresponding function/hook event. There is no need for that and it creates various complications in the processing of the proof hint trace. For this reason, this PR un-nests those events so that they appear before their corresponding function/hook event.

theo25 commented 2 months ago

@Robertorosmaninho I added a commit with the update and a simplification to the parser logic. Thanks for pointing that out!

Robertorosmaninho commented 2 months ago

@Robertorosmaninho I added a commit with the update and a simplification to the parser logic. Thanks for pointing that out!

Wow! That was a huge simplification! Thanks!