FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
394 stars 58 forks source link

Fix spinlock extraction due to stronger monomorphization #438

Closed R1kM closed 3 months ago

R1kM commented 3 months ago

431 introduced a stronger monomorphization, which in particular rewrites occurences of Steel_SpinLock_lock () into Steel_SpinLock_s_lock. This in turn leads to escaping the address-passing semantics of locks.

This PR fixes this by adding Steel_SpinLock_s_lock to the specific handling of locks.

msprotz commented 3 months ago

nice find -- great!!