Improvements to MINT hooks

runtimeverification / llvm-backend

KORE to llvm translation

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

36 stars 23 forks source link

Closed dwightguth closed 3 months ago

dwightguth commented 3 months ago

This PR contains a couple different small changes to improve support for MInt in the WASM semantics:

Add implementation of MINT.round, MINT.sext, MINT.umin, MINT.umax, MINT.smin, and MINT.smax.
Add support for equality between machine integers of size 32 and 64 bits.
Add variant of hook_LIST_update which takes an MInt.