search

runtimeverification / wasm-semantics

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

use optimization level 3 for llvm backend #648

Closed dwightguth closed 3 weeks ago

dwightguth commented 3 weeks ago

We pass -O3 to kompile instead of -O2 in order to decrease time spent doing pattern matching in the llvm backend.

dwightguth commented 3 weeks ago

Yes, the intention is that this optimization change has no impact on the transition system, and we've pretty much ironed out the rest of the bugs at this point. It makes the binary bigger, but not overly so.