runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
74 stars 18 forks source link

Definedness improvements #651

Closed bbyalcinkaya closed 2 weeks ago

bbyalcinkaya commented 3 weeks ago
jberthold commented 2 weeks ago

FYI I am running a test with these changes (even though the calls are not protected against arguments being negative yet). My test includes another small change (marking the load instruction for signed result as preserving definedness). Maybe you could consider adding it to this PR, or I can open another one.